Theorem eqeltrid 2292

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 2282	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eqeltrrid  2293  csbexga  4173  rabexd  4190  otexg  4275  tpexg  4492  dmresexg  4983  f1oabexg  5536  funfvex  5595  riotaexg  5905  riotaprop  5925  fnovex  5979  ovexg  5980  fovcdm  6091  fnovrn  6096  cofunexg  6196  cofunex2g  6197  abrexex2g  6207  xpexgALT  6220  mpofvex  6293  tfrex  6456  frec0g  6485  freccllem  6490  ecexg  6626  qsexg  6680  pmex  6742  elixpsn  6824  diffifi  6993  unfidisj  7021  prfidisj  7026  tpfidisj  7028  tpfidceq  7029  ssfirab  7035  ssfidc  7036  fnfi  7040  funrnfi  7046  iunfidisj  7050  infclti  7127  supex2g  7137  infex2g  7138  djuex  7147  ctssdccl  7215  addvalex  7959  negcl  8274  intqfrac2  10466  intfracq  10467  frec2uzzd  10547  frecuzrdgrrn  10555  iseqf1olemqpcl  10656  seq3f1olemqsum  10660  seqf1oglem1  10666  seqf1oglem2  10667  bcval5  10910  xrmaxiflemval  11594  climmpt  11644  reccn2ap  11657  zsumdc  11728  fsumzcl2  11749  fsump1i  11777  fsumabs  11809  hash2iun1dif1  11824  mertenslemi1  11879  fprodcllemf  11957  bitsfzolem  12298  nninfctlemfo  12394  algrf  12400  algcvg  12403  algcvga  12406  algfx  12407  eucalgcvga  12413  eucalg  12414  crth  12579  phimullem  12580  eulerthlemth  12587  prmdiv  12590  pythagtriplem11  12630  pythagtriplem13  12632  pcprecl  12645  infpnlem1  12715  infpnlem2  12716  4sqlem5  12738  mul4sqlem  12749  4sqlemafi  12751  4sqlem13m  12759  4sqlem14  12760  4sqlem17  12763  4sqlem18  12764  ennnfonelemj0  12805  ennnfonelemom  12812  ressbasid  12935  ressval3d  12937  1strbas  12982  2strbasg  12985  2stropg  12986  restid  13115  topnvalg  13116  topnidg  13117  prdsval  13138  prdsplusg  13142  prdsmulr  13143  pwsval  13156  pwselbasb  13158  pwssnf1o  13163  imasival  13171  imasmulr  13174  imasaddfn  13182  imasaddval  13183  imasaddf  13184  imasmulfn  13185  imasmulval  13186  imasmulf  13187  qusval  13188  qusaddval  13200  qusaddf  13201  qusmulval  13202  qusmulf  13203  xpsval  13217  plusffvalg  13227  plusfvalg  13228  grpidvalg  13238  igsumvalx  13254  gsumfzval  13256  gsum0g  13261  gsumsplit1r  13263  gsumprval  13264  prdssgrpd  13280  issubmnd  13307  ress0g  13308  ismhm  13326  0mhm  13351  grpinvfvalg  13407  grpinvval  13408  grpinvfng  13409  grpsubfvalg  13410  grpsubval  13411  grpressid  13426  grplactfval  13466  prdsinvlem  13473  mulgfvalg  13490  mulgval  13491  mulgfng  13493  mulgnngsum  13496  mulgnnp1  13499  mulgnndir  13520  issubg  13542  subggrp  13546  issubg2m  13558  eqgfval  13591  eqgen  13596  quselbasg  13599  quseccl0g  13600  isghm  13612  ghmima  13634  ablressid  13704  gsumfzmptfidmadd  13708  mgpvalg  13718  mgpplusgg  13719  mgptopng  13724  mgpress  13726  rngressid  13749  issrg  13760  ringidss  13824  ring1  13854  ringressid  13858  opprvalg  13864  opprmulfvalg  13865  rdivmuldivd  13939  isnzr2  13979  issubrg  14016  subrgring  14019  rrgval  14057  islmod  14086  scaffvalg  14101  scafvalg  14102  lsssetm  14151  islssm  14152  islssmg  14153  lss1d  14178  lspfval  14183  lspval  14185  lspcl  14186  ellspsn  14212  rnglidlmmgm  14291  rnglidlmsgrp  14292  2idlval  14297  2idlvalg  14298  qusrhm  14323  zlmval  14422  zlmvscag  14428  znval  14431  znle  14432  znbaslemnn  14434  znbas  14439  znzrhval  14442  znleval  14448  psrval  14461  psrbasg  14469  psrelbas  14470  psrplusgg  14473  mplvalcoe  14485  mplbascoe  14486  mplplusgg  14498  topopn  14513  topcld  14614  uncld  14618  iuncld  14620  unicld  14621  tgrest  14674  restin  14681  cnco  14726  cnrest  14740  cnptoprest2  14745  lmss  14751  txbasval  14772  txcn  14780  cnmpt12f  14791  hmeoco  14821  idhmeo  14822  blres  14939  metrest  15011  qtopbasss  15026  tgqioo  15060  divcnap  15070  fsumcncntop  15072  cncfmet  15097  sub1cncf  15107  sub2cncf  15108  cdivcncfap  15109  cnrehmeocntop  15115  cnplimcim  15172  limccnpcntop  15180  limccnp2lem  15181  limccnp2cntop  15182  dvfvalap  15186  dvidsslem  15198  dvmptfsum  15230  plyid  15251  fsumdvdsmul  15496  gausslemma2dlem0b  15560  gausslemma2dlem0d  15562  gausslemma2dlem0h  15566  gausslemma2dlem5a  15575  gausslemma2dlem5  15576  gausslemma2dlem6  15577  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisenlem4  15583  2lgslem2  15602  2sqlem8  15633  struct2slots2dom  15668  structiedg0val  15670  edgstruct  15691  bj-snexg  15885  trilpolemcl  16013