Theorem syl5eqel 1552

Description: A membership and equality inference.

Hypotheses

Ref	Expression
syl5eqel.1	|- (ph -> A e. B)
syl5eqel.2	|- C = A

Assertion

Ref	Expression
syl5eqel	|- (ph -> C e. B)

Proof of Theorem syl5eqel

Step	Hyp	Ref	Expression
1		syl5eqel.2	. . 3 |- C = A
2	1	a1i 8	. 2 |- (ph -> C = A)
3		syl5eqel.1	. 2 |- (ph -> A e. B)
4	2, 3	eqeltrd 1548	1 |- (ph -> C e. B)

Syntax hints:   -> wi 3   = wceq 956   e. wcel 958

This theorem is referenced by:  syl5eqelr 1553  csbexg 2008  abssexg 2747  dmresexg 3382  resexg 3394  cofunexg 3580  cofunex2g 3581  f1oabexg 3700  iunon 3909  iinon 3910  oprabex2g 4020  foprrn 4035  fnoprvalrn 4038  oelim2 4222  ecexg 4265  pmex 4327  supcl 4579  rankelpr 4708  rankelop 4709  scott0 4717  htalem 4727  negclt 5368  uzwo3lem2 6217  quoremz 6251  intfrac 6253  intfracOLD 6254  intfracqOLD 6255  seq1rn2 6321  discrlem2 6657  discrlem3 6658  ser0clt 7046  ser1clt 7047  ser1cmp2lem 7176  ser1cmp2 7177  iserzabslem 7178  isumclt 7209  ivthlem7 7287  efclt 7312  efcnlem2 7420  acdc3lem 7486  acdc2lem2 7489  acdc5lem2 7492  acdclem 7494  infpnlem1 7506  infpnlem2 7507  topopn 7602  indistop 7648  cldval 7666  ntrfval 7667  clsfval 7668  iscld 7669  topcld 7675  ntrval 7676  clsval 7677  intcld 7680  uncld 7681  elcls3 7711  neifval 7714  neif 7715  neiss2 7716  neival 7717  isnei 7718  lpfval 7742  lpval 7743  islp2 7747  iscn 7758  iscnp 7760  cnco 7768  metxplem1 7826  metxplem2 7827  blfval 7835  blval 7837  blrn 7841  blf 7844  opnfval 7857  isopn 7859  lmfval 7925  caufval 7926  lmbr 7928  iscau 7936  fsumcnlem 7989  bcthlem9 8007  grpidval 8058  grpinvfval 8066  grpinvval 8067  grpinvf 8079  grpdivfval 8081  grplactfval 8096  issubg 8116  isvc 8200  isnv 8231  imsmet 8324  ubthlem7 8535  ubthlem10 8538  spwval2 8653  pjthlem2 9220  pjthlem4 9222  pjoc1 9264  osum 9586  nmcopexlem4 9954  nmcfnexlem4 9983  cnlnadjlem3 10002  mdsymlem1 10330  mdsymlem3 10332  ghomgrp 10390  inpws2 10456  fnoprvalrn2 10470  mapudiscn 10512  homeofval 10516  idhme 10522  hmphre 10530  homcardus 10540  qusp 10555  sfvlim 10605  sfvlimOLD 10606

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472

Copyright terms: Public domain