Theorem eqeltrid 2257

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

Hypotheses

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

Assertion

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

Proof of Theorem eqeltrid

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

Syntax hints:   -> wi 4   = wceq 1348   e. wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eqeltrrid  2258  csbexga  4115  otexg  4213  tpexg  4427  dmresexg  4912  f1oabexg  5452  funfvex  5511  riotaexg  5811  riotaprop  5830  fnovex  5884  ovexg  5885  fovrn  5993  fnovrn  5998  cofunexg  6086  cofunex2g  6087  abrexex2g  6097  xpexgALT  6110  mpofvex  6180  tfrex  6345  frec0g  6374  freccllem  6379  ecexg  6515  qsexg  6567  pmex  6629  elixpsn  6711  diffifi  6870  unfidisj  6897  prfidisj  6902  tpfidisj  6903  ssfirab  6909  ssfidc  6910  fnfi  6912  funrnfi  6917  iunfidisj  6921  infclti  6998  supex2g  7008  infex2g  7009  djuex  7018  ctssdccl  7086  addvalex  7799  negcl  8112  intqfrac2  10268  intfracq  10269  frec2uzzd  10349  frecuzrdgrrn  10357  iseqf1olemqpcl  10445  seq3f1olemqsum  10449  bcval5  10690  xrmaxiflemval  11206  climmpt  11256  reccn2ap  11269  zsumdc  11340  fsumzcl2  11361  fsump1i  11389  fsumabs  11421  hash2iun1dif1  11436  mertenslemi1  11491  fprodcllemf  11569  algrf  11992  algcvg  11995  algcvga  11998  algfx  11999  eucalgcvga  12005  eucalg  12006  crth  12171  phimullem  12172  eulerthlemth  12179  prmdiv  12182  pythagtriplem11  12221  pythagtriplem13  12223  pcprecl  12236  infpnlem1  12304  infpnlem2  12305  4sqlem5  12327  mul4sqlem  12338  ennnfonelemj0  12349  ennnfonelemom  12356  ressid  12472  1strbas  12510  2strbasg  12512  2stropg  12513  restid  12583  topnvalg  12584  topnidg  12585  plusffvalg  12609  plusfvalg  12610  grpidvalg  12620  ismhm  12678  0mhm  12697  topopn  12765  topcld  12868  uncld  12872  iuncld  12874  unicld  12875  tgrest  12928  restin  12935  cnco  12980  cnrest  12994  cnptoprest2  12999  lmss  13005  txbasval  13026  txcn  13034  cnmpt12f  13045  hmeoco  13075  idhmeo  13076  blres  13193  metrest  13265  qtopbasss  13280  tgqioo  13306  divcnap  13314  fsumcncntop  13315  cncfmet  13338  cdivcncfap  13346  cnrehmeocntop  13352  cnplimcim  13395  limccnpcntop  13403  limccnp2lem  13404  limccnp2cntop  13405  dvfvalap  13409  2sqlem8  13718  bj-snexg  13912  trilpolemcl  14034