Theorem eqeltrid 2318

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eqeltrrid  2319  csbexga  4217  rabexd  4235  otexg  4322  tpexg  4541  dmresexg  5036  f1oabexg  5595  funfvex  5656  elfvfvex  5673  riotaexg  5975  riotaeqimp  5996  riotaprop  5997  fnovex  6051  ovexg  6052  elovimad  6062  fovcdm  6165  fnovrn  6170  cofunexg  6271  cofunex2g  6272  abrexex2g  6282  xpexgALT  6295  mpofvex  6370  tfrex  6534  frec0g  6563  freccllem  6568  ecexg  6706  qsexg  6760  pmex  6822  elixpsn  6904  diffifi  7083  unfidisj  7114  prfidisj  7119  tpfidisj  7121  tpfidceq  7122  ssfirab  7129  ssfidc  7130  fnfi  7135  funrnfi  7141  iunfidisj  7145  infclti  7222  supex2g  7232  infex2g  7233  djuex  7242  ctssdccl  7310  addvalex  8064  negcl  8379  intqfrac2  10582  intfracq  10583  frec2uzzd  10663  frecuzrdgrrn  10671  iseqf1olemqpcl  10772  seq3f1olemqsum  10776  seqf1oglem1  10782  seqf1oglem2  10783  bcval5  11026  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12  11318  pfxccat3  11319  pfxccatpfx2  11322  pfxccat3a  11323  swrdccat3blem  11324  swrdccat3b  11325  cats1cld  11348  xrmaxiflemval  11828  climmpt  11878  reccn2ap  11891  zsumdc  11963  fsumzcl2  11984  fsump1i  12012  fsumabs  12044  hash2iun1dif1  12059  mertenslemi1  12114  fprodcllemf  12192  bitsfzolem  12533  nninfctlemfo  12629  algrf  12635  algcvg  12638  algcvga  12641  algfx  12642  eucalgcvga  12648  eucalg  12649  crth  12814  phimullem  12815  eulerthlemth  12822  prmdiv  12825  pythagtriplem11  12865  pythagtriplem13  12867  pcprecl  12880  infpnlem1  12950  infpnlem2  12951  4sqlem5  12973  mul4sqlem  12984  4sqlemafi  12986  4sqlem13m  12994  4sqlem14  12995  4sqlem17  12998  4sqlem18  12999  ennnfonelemj0  13040  ennnfonelemom  13047  ressbasid  13171  ressval3d  13173  1strbas  13218  2strbasg  13221  2stropg  13222  restid  13351  topnvalg  13352  topnidg  13353  prdsval  13374  prdsplusg  13378  prdsmulr  13379  pwsval  13392  pwselbasb  13394  pwssnf1o  13399  imasival  13407  imasmulr  13410  imasaddfn  13418  imasaddval  13419  imasaddf  13420  imasmulfn  13421  imasmulval  13422  imasmulf  13423  qusval  13424  qusaddval  13436  qusaddf  13437  qusmulval  13438  qusmulf  13439  xpsval  13453  plusffvalg  13463  plusfvalg  13464  grpidvalg  13474  igsumvalx  13490  gsumfzval  13492  gsum0g  13497  gsumsplit1r  13499  gsumprval  13500  prdssgrpd  13516  issubmnd  13543  ress0g  13544  ismhm  13562  0mhm  13587  grpinvfvalg  13643  grpinvval  13644  grpinvfng  13645  grpsubfvalg  13646  grpsubval  13647  grpressid  13662  grplactfval  13702  prdsinvlem  13709  mulgfvalg  13726  mulgval  13727  mulgfng  13729  mulgnngsum  13732  mulgnnp1  13735  mulgnndir  13756  issubg  13778  subggrp  13782  issubg2m  13794  eqgfval  13827  eqgen  13832  quselbasg  13835  quseccl0g  13836  isghm  13848  ghmima  13870  ablressid  13940  gsumfzmptfidmadd  13944  mgpvalg  13955  mgpplusgg  13956  mgptopng  13961  mgpress  13963  rngressid  13986  issrg  13997  ringidss  14061  ring1  14091  ringressid  14095  opprvalg  14101  opprmulfvalg  14102  rdivmuldivd  14177  isnzr2  14217  issubrg  14254  subrgring  14257  rrgval  14295  islmod  14324  scaffvalg  14339  scafvalg  14340  lsssetm  14389  islssm  14390  islssmg  14391  lss1d  14416  lspfval  14421  lspval  14423  lspcl  14424  ellspsn  14450  rnglidlmmgm  14529  rnglidlmsgrp  14530  2idlval  14535  2idlvalg  14536  qusrhm  14561  zlmval  14660  zlmvscag  14666  znval  14669  znle  14670  znbaslemnn  14672  znbas  14677  znzrhval  14680  znleval  14686  psrval  14699  psrbasg  14707  psrelbas  14708  psrplusgg  14711  mplvalcoe  14723  mplbascoe  14724  mplplusgg  14736  topopn  14751  topcld  14852  uncld  14856  iuncld  14858  unicld  14859  tgrest  14912  restin  14919  cnco  14964  cnrest  14978  cnptoprest2  14983  lmss  14989  txbasval  15010  txcn  15018  cnmpt12f  15029  hmeoco  15059  idhmeo  15060  blres  15177  metrest  15249  qtopbasss  15264  tgqioo  15298  divcnap  15308  fsumcncntop  15310  cncfmet  15335  sub1cncf  15345  sub2cncf  15346  cdivcncfap  15347  cnrehmeocntop  15353  cnplimcim  15410  limccnpcntop  15418  limccnp2lem  15419  limccnp2cntop  15420  dvfvalap  15424  dvidsslem  15436  dvmptfsum  15468  plyid  15489  fsumdvdsmul  15734  gausslemma2dlem0b  15798  gausslemma2dlem0d  15800  gausslemma2dlem0h  15804  gausslemma2dlem5a  15813  gausslemma2dlem5  15814  gausslemma2dlem6  15815  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  2lgslem2  15840  2sqlem8  15871  struct2slots2dom  15908  structiedg0val  15910  edgstruct  15934  uhgrunop  15957  incistruhgr  15960  upgrunop  15997  umgrunop  15999  usgredg2v  16094  usgriedgdomord  16095  uspgredgdomord  16099  subgruhgredgdm  16140  uhgrspansubgrlem  16146  uhgrspanop  16152  upgrspanop  16153  umgrspanop  16154  usgrspanop  16155  vtxdgfval  16158  wksfval  16192  wlk1walkdom  16229  clwwlkg  16263  trlsegvdeglem3  16332  trlsegvdeglem5  16334  eupthvdres  16345  eupth2lem3fi  16346  eupth2lembfi  16347  bj-snexg  16558  trilpolemcl  16692  gsumgfsumlem  16735  gfsumcl  16739