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  5974  riotaeqimp  5995  riotaprop  5996  fnovex  6050  ovexg  6051  elovimad  6061  fovcdm  6164  fnovrn  6169  cofunexg  6270  cofunex2g  6271  abrexex2g  6281  xpexgALT  6294  mpofvex  6369  tfrex  6533  frec0g  6562  freccllem  6567  ecexg  6705  qsexg  6759  pmex  6821  elixpsn  6903  diffifi  7082  unfidisj  7113  prfidisj  7118  tpfidisj  7120  tpfidceq  7121  ssfirab  7128  ssfidc  7129  fnfi  7134  funrnfi  7140  iunfidisj  7144  infclti  7221  supex2g  7231  infex2g  7232  djuex  7241  ctssdccl  7309  addvalex  8063  negcl  8378  intqfrac2  10580  intfracq  10581  frec2uzzd  10661  frecuzrdgrrn  10669  iseqf1olemqpcl  10770  seq3f1olemqsum  10774  seqf1oglem1  10780  seqf1oglem2  10781  bcval5  11024  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12  11313  pfxccat3  11314  pfxccatpfx2  11317  pfxccat3a  11318  swrdccat3blem  11319  swrdccat3b  11320  cats1cld  11343  xrmaxiflemval  11810  climmpt  11860  reccn2ap  11873  zsumdc  11944  fsumzcl2  11965  fsump1i  11993  fsumabs  12025  hash2iun1dif1  12040  mertenslemi1  12095  fprodcllemf  12173  bitsfzolem  12514  nninfctlemfo  12610  algrf  12616  algcvg  12619  algcvga  12622  algfx  12623  eucalgcvga  12629  eucalg  12630  crth  12795  phimullem  12796  eulerthlemth  12803  prmdiv  12806  pythagtriplem11  12846  pythagtriplem13  12848  pcprecl  12861  infpnlem1  12931  infpnlem2  12932  4sqlem5  12954  mul4sqlem  12965  4sqlemafi  12967  4sqlem13m  12975  4sqlem14  12976  4sqlem17  12979  4sqlem18  12980  ennnfonelemj0  13021  ennnfonelemom  13028  ressbasid  13152  ressval3d  13154  1strbas  13199  2strbasg  13202  2stropg  13203  restid  13332  topnvalg  13333  topnidg  13334  prdsval  13355  prdsplusg  13359  prdsmulr  13360  pwsval  13373  pwselbasb  13375  pwssnf1o  13380  imasival  13388  imasmulr  13391  imasaddfn  13399  imasaddval  13400  imasaddf  13401  imasmulfn  13402  imasmulval  13403  imasmulf  13404  qusval  13405  qusaddval  13417  qusaddf  13418  qusmulval  13419  qusmulf  13420  xpsval  13434  plusffvalg  13444  plusfvalg  13445  grpidvalg  13455  igsumvalx  13471  gsumfzval  13473  gsum0g  13478  gsumsplit1r  13480  gsumprval  13481  prdssgrpd  13497  issubmnd  13524  ress0g  13525  ismhm  13543  0mhm  13568  grpinvfvalg  13624  grpinvval  13625  grpinvfng  13626  grpsubfvalg  13627  grpsubval  13628  grpressid  13643  grplactfval  13683  prdsinvlem  13690  mulgfvalg  13707  mulgval  13708  mulgfng  13710  mulgnngsum  13713  mulgnnp1  13716  mulgnndir  13737  issubg  13759  subggrp  13763  issubg2m  13775  eqgfval  13808  eqgen  13813  quselbasg  13816  quseccl0g  13817  isghm  13829  ghmima  13851  ablressid  13921  gsumfzmptfidmadd  13925  mgpvalg  13935  mgpplusgg  13936  mgptopng  13941  mgpress  13943  rngressid  13966  issrg  13977  ringidss  14041  ring1  14071  ringressid  14075  opprvalg  14081  opprmulfvalg  14082  rdivmuldivd  14157  isnzr2  14197  issubrg  14234  subrgring  14237  rrgval  14275  islmod  14304  scaffvalg  14319  scafvalg  14320  lsssetm  14369  islssm  14370  islssmg  14371  lss1d  14396  lspfval  14401  lspval  14403  lspcl  14404  ellspsn  14430  rnglidlmmgm  14509  rnglidlmsgrp  14510  2idlval  14515  2idlvalg  14516  qusrhm  14541  zlmval  14640  zlmvscag  14646  znval  14649  znle  14650  znbaslemnn  14652  znbas  14657  znzrhval  14660  znleval  14666  psrval  14679  psrbasg  14687  psrelbas  14688  psrplusgg  14691  mplvalcoe  14703  mplbascoe  14704  mplplusgg  14716  topopn  14731  topcld  14832  uncld  14836  iuncld  14838  unicld  14839  tgrest  14892  restin  14899  cnco  14944  cnrest  14958  cnptoprest2  14963  lmss  14969  txbasval  14990  txcn  14998  cnmpt12f  15009  hmeoco  15039  idhmeo  15040  blres  15157  metrest  15229  qtopbasss  15244  tgqioo  15278  divcnap  15288  fsumcncntop  15290  cncfmet  15315  sub1cncf  15325  sub2cncf  15326  cdivcncfap  15327  cnrehmeocntop  15333  cnplimcim  15390  limccnpcntop  15398  limccnp2lem  15399  limccnp2cntop  15400  dvfvalap  15404  dvidsslem  15416  dvmptfsum  15448  plyid  15469  fsumdvdsmul  15714  gausslemma2dlem0b  15778  gausslemma2dlem0d  15780  gausslemma2dlem0h  15784  gausslemma2dlem5a  15793  gausslemma2dlem5  15794  gausslemma2dlem6  15795  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  2lgslem2  15820  2sqlem8  15851  struct2slots2dom  15888  structiedg0val  15890  edgstruct  15914  uhgrunop  15937  incistruhgr  15940  upgrunop  15977  umgrunop  15979  usgredg2v  16074  usgriedgdomord  16075  uspgredgdomord  16079  subgruhgredgdm  16120  uhgrspansubgrlem  16126  uhgrspanop  16132  upgrspanop  16133  umgrspanop  16134  usgrspanop  16135  vtxdgfval  16138  wksfval  16172  wlk1walkdom  16209  clwwlkg  16243  trlsegvdeglem3  16312  trlsegvdeglem5  16314  bj-snexg  16507  trilpolemcl  16641  gsumgfsumlem  16683