Theorem syl5eqel 2174

Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

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

Assertion

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

Proof of Theorem syl5eqel

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

Syntax hints:   -> wi 4   = wceq 1289   e. wcel 1438

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084

This theorem is referenced by:  syl5eqelr  2175  csbexga  3967  otexg  4057  tpexg  4269  dmresexg  4736  f1oabexg  5265  funfvex  5322  riotaexg  5612  riotaprop  5631  fnovex  5682  ovexg  5683  fovrn  5787  fnovrn  5792  cofunexg  5882  cofunex2g  5883  abrexex2g  5891  xpexgALT  5904  mpt2fvex  5973  tfrex  6133  frec0g  6162  freccllem  6167  ecexg  6294  qsexg  6346  pmex  6408  diffifi  6608  unfidisj  6630  prfidisj  6635  tpfidisj  6636  ssfirab  6641  ssfidc  6642  fnfi  6644  funrnfi  6649  iunfidisj  6653  infclti  6716  djuex  6734  addvalex  7379  negcl  7680  intqfrac2  9722  intfracq  9723  frec2uzzd  9803  frecuzrdgrrn  9811  iseqf1olemqpcl  9921  seq3f1olemqsum  9925  ibcval5  10167  climmpt  10684  zisum  10770  fsumzcl2  10795  fsump1i  10823  fsumabs  10855  hash2iun1dif1  10870  mertenslemi1  10925  ialgcvg  11304  ialgcvga  11307  ialgfx  11308  eucialgcvga  11314  eucialg  11315  crth  11474  phimullem  11475  ressid  11548  topopn  11560  bj-snexg  11758