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  4172  rabexd  4189  otexg  4274  tpexg  4491  dmresexg  4982  f1oabexg  5534  funfvex  5593  riotaexg  5903  riotaprop  5923  fnovex  5977  ovexg  5978  fovcdm  6089  fnovrn  6094  cofunexg  6194  cofunex2g  6195  abrexex2g  6205  xpexgALT  6218  mpofvex  6291  tfrex  6454  frec0g  6483  freccllem  6488  ecexg  6624  qsexg  6678  pmex  6740  elixpsn  6822  diffifi  6991  unfidisj  7019  prfidisj  7024  tpfidisj  7026  tpfidceq  7027  ssfirab  7033  ssfidc  7034  fnfi  7038  funrnfi  7044  iunfidisj  7048  infclti  7125  supex2g  7135  infex2g  7136  djuex  7145  ctssdccl  7213  addvalex  7957  negcl  8272  intqfrac2  10464  intfracq  10465  frec2uzzd  10545  frecuzrdgrrn  10553  iseqf1olemqpcl  10654  seq3f1olemqsum  10658  seqf1oglem1  10664  seqf1oglem2  10665  bcval5  10908  xrmaxiflemval  11561  climmpt  11611  reccn2ap  11624  zsumdc  11695  fsumzcl2  11716  fsump1i  11744  fsumabs  11776  hash2iun1dif1  11791  mertenslemi1  11846  fprodcllemf  11924  bitsfzolem  12265  nninfctlemfo  12361  algrf  12367  algcvg  12370  algcvga  12373  algfx  12374  eucalgcvga  12380  eucalg  12381  crth  12546  phimullem  12547  eulerthlemth  12554  prmdiv  12557  pythagtriplem11  12597  pythagtriplem13  12599  pcprecl  12612  infpnlem1  12682  infpnlem2  12683  4sqlem5  12705  mul4sqlem  12716  4sqlemafi  12718  4sqlem13m  12726  4sqlem14  12727  4sqlem17  12730  4sqlem18  12731  ennnfonelemj0  12772  ennnfonelemom  12779  ressbasid  12902  ressval3d  12904  1strbas  12949  2strbasg  12952  2stropg  12953  restid  13082  topnvalg  13083  topnidg  13084  prdsval  13105  prdsplusg  13109  prdsmulr  13110  pwsval  13123  pwselbasb  13125  pwssnf1o  13130  imasival  13138  imasmulr  13141  imasaddfn  13149  imasaddval  13150  imasaddf  13151  imasmulfn  13152  imasmulval  13153  imasmulf  13154  qusval  13155  qusaddval  13167  qusaddf  13168  qusmulval  13169  qusmulf  13170  xpsval  13184  plusffvalg  13194  plusfvalg  13195  grpidvalg  13205  igsumvalx  13221  gsumfzval  13223  gsum0g  13228  gsumsplit1r  13230  gsumprval  13231  prdssgrpd  13247  issubmnd  13274  ress0g  13275  ismhm  13293  0mhm  13318  grpinvfvalg  13374  grpinvval  13375  grpinvfng  13376  grpsubfvalg  13377  grpsubval  13378  grpressid  13393  grplactfval  13433  prdsinvlem  13440  mulgfvalg  13457  mulgval  13458  mulgfng  13460  mulgnngsum  13463  mulgnnp1  13466  mulgnndir  13487  issubg  13509  subggrp  13513  issubg2m  13525  eqgfval  13558  eqgen  13563  quselbasg  13566  quseccl0g  13567  isghm  13579  ghmima  13601  ablressid  13671  gsumfzmptfidmadd  13675  mgpvalg  13685  mgpplusgg  13686  mgptopng  13691  mgpress  13693  rngressid  13716  issrg  13727  ringidss  13791  ring1  13821  ringressid  13825  opprvalg  13831  opprmulfvalg  13832  rdivmuldivd  13906  isnzr2  13946  issubrg  13983  subrgring  13986  rrgval  14024  islmod  14053  scaffvalg  14068  scafvalg  14069  lsssetm  14118  islssm  14119  islssmg  14120  lss1d  14145  lspfval  14150  lspval  14152  lspcl  14153  ellspsn  14179  rnglidlmmgm  14258  rnglidlmsgrp  14259  2idlval  14264  2idlvalg  14265  qusrhm  14290  zlmval  14389  zlmvscag  14395  znval  14398  znle  14399  znbaslemnn  14401  znbas  14406  znzrhval  14409  znleval  14415  psrval  14428  psrbasg  14436  psrelbas  14437  psrplusgg  14440  mplvalcoe  14452  mplbascoe  14453  mplplusgg  14465  topopn  14480  topcld  14581  uncld  14585  iuncld  14587  unicld  14588  tgrest  14641  restin  14648  cnco  14693  cnrest  14707  cnptoprest2  14712  lmss  14718  txbasval  14739  txcn  14747  cnmpt12f  14758  hmeoco  14788  idhmeo  14789  blres  14906  metrest  14978  qtopbasss  14993  tgqioo  15027  divcnap  15037  fsumcncntop  15039  cncfmet  15064  sub1cncf  15074  sub2cncf  15075  cdivcncfap  15076  cnrehmeocntop  15082  cnplimcim  15139  limccnpcntop  15147  limccnp2lem  15148  limccnp2cntop  15149  dvfvalap  15153  dvidsslem  15165  dvmptfsum  15197  plyid  15218  fsumdvdsmul  15463  gausslemma2dlem0b  15527  gausslemma2dlem0d  15529  gausslemma2dlem0h  15533  gausslemma2dlem5a  15542  gausslemma2dlem5  15543  gausslemma2dlem6  15544  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  2lgslem2  15569  2sqlem8  15600  struct2slots2dom  15635  structiedg0val  15637  edgstruct  15656  bj-snexg  15848  trilpolemcl  15976