Theorem eqeltrid 2325

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

Syntax hints:   -> wi 4   = wceq 1402   e. wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  eqeltrrid  2326  csbexga  4256  rabexd  4276  otexg  4365  tpexg  4585  dmresexg  5081  f1oabexg  5646  funfvex  5707  elfvfvex  5724  riotaexg  6032  riotaeqimp  6053  riotaprop  6054  fnovex  6108  ovexg  6109  elovimad  6119  fovcdm  6222  fnovrn  6227  cofunexg  6328  cofunex2g  6329  abrexex2g  6339  xpexgALT  6356  mpofvex  6431  mptsuppdifd  6485  tfrex  6629  frec0g  6658  freccllem  6663  ecexg  6801  qsexg  6855  pmex  6917  elixpsn  7007  diffifi  7188  unfidisj  7219  prfidisj  7224  tpfidisj  7226  tpfidceq  7227  ssfirab  7234  ssfidc  7235  fnfi  7240  funrnfi  7246  iunfidisj  7250  infclti  7353  supex2g  7363  infex2g  7364  djuex  7373  ctssdccl  7441  addvalex  8201  negcl  8516  intqfrac2  10734  intfracq  10735  frec2uzzd  10815  frecuzrdgrrn  10823  iseqf1olemqpcl  10924  seq3f1olemqsum  10928  seqf1oglem1  10934  seqf1oglem2  10935  bcval5  11179  hashf1lem2  11264  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12  11483  pfxccat3  11484  pfxccatpfx2  11487  pfxccat3a  11488  swrdccat3blem  11489  swrdccat3b  11490  cats1cld  11513  xrmaxiflemval  11994  climmpt  12044  reccn2ap  12057  zsumdc  12129  fsumzcl2  12150  fsump1i  12178  fsumabs  12210  hash2iun1dif1  12225  mertenslemi1  12280  fprodcllemf  12358  bitsfzolem  12699  nninfctlemfo  12795  algrf  12801  algcvg  12804  algcvga  12807  algfx  12808  eucalgcvga  12814  eucalg  12815  crth  12980  phimullem  12981  eulerthlemth  12988  prmdiv  12991  pythagtriplem11  13031  pythagtriplem13  13033  pcprecl  13046  infpnlem1  13116  infpnlem2  13117  4sqlem5  13139  mul4sqlem  13150  4sqlemafi  13152  4sqlem13m  13160  4sqlem14  13161  4sqlem17  13164  4sqlem18  13165  ennnfonelemj0  13270  ennnfonelemom  13277  ressbasid  13401  ressval3d  13403  1strbas  13448  2strbasg  13451  2stropg  13452  restid  13581  topnvalg  13582  topnidg  13583  imasival  13604  imasmulr  13607  imasaddfn  13615  imasaddval  13616  imasaddf  13617  imasmulfn  13618  imasmulval  13619  imasmulf  13620  qusval  13621  qusaddval  13633  qusaddf  13634  qusmulval  13635  qusmulf  13636  plusffvalg  13659  plusfvalg  13660  grpidvalg  13670  gzsumvalx  13686  gzsumfzval  13688  gzsum0  13690  gzsumsplit1r  13692  issubmnd  13732  ress0g  13733  ismhm  13745  0mhm  13770  grpinvfvalg  13824  grpinvval  13825  grpinvfng  13826  grpsubfvalg  13827  grpsubval  13828  grpressid  13843  grplactfval  13883  mulgfvalg  13901  mulgval  13902  mulgfng  13904  mulgnngzsum  13907  mulgnnp1  13910  mulgnndir  13931  issubg  13953  subggrp  13957  issubg2m  13969  eqgfval  14002  eqgen  14007  quselbasg  14010  quseccl0g  14011  isghm  14023  ghmima  14045  ablressid  14116  gzsumshift  14126  gsumclfi  14136  gsumsubmclfi  14140  prdsval  14150  prdsplusg  14154  prdsmulr  14155  prdssgrpd  14168  prdsinvlem  14173  xpsval  14178  pwsval  14181  pwselbasb  14183  pwssnf1o  14188  mgpvalg  14197  mgpplusgg  14198  mgptopng  14203  mgpress  14205  rngressid  14228  issrg  14243  ringidss  14307  ring1  14337  ringressid  14341  opprvalg  14347  opprmulfvalg  14348  rdivmuldivd  14424  isnzr2  14464  issubrg  14502  subrgring  14505  rrgval  14543  islmod  14600  scaffvalg  14615  scafvalg  14616  lsssetm  14665  islssm  14666  islssmg  14667  lss1d  14692  lspfval  14697  lspval  14699  lspcl  14700  ellspsn  14726  rnglidlmmgm  14805  rnglidlmsgrp  14806  2idlval  14811  2idlvalg  14812  qusrhm  14837  zlmval  14934  zlmvscag  14940  znval  14943  znle  14944  znbaslemnn  14946  znbas  14951  znzrhval  14954  znleval  14960  psrval  14973  psrbasg  14988  psrelbas  14989  psrplusgg  14992  mplvalcoe  15004  mplbascoe  15005  mplplusgg  15017  topopn  15032  topcld  15133  uncld  15137  iuncld  15139  unicld  15140  tgrest  15193  restin  15200  cnco  15245  cnrest  15259  cnptoprest2  15264  lmss  15270  txbasval  15291  txcn  15299  cnmpt12f  15310  hmeoco  15340  idhmeo  15341  blres  15458  metrest  15530  qtopbasss  15545  tgqioo  15579  divcnap  15589  fsumcncntop  15591  cncfmet  15616  sub1cncf  15626  sub2cncf  15627  cdivcncfap  15628  cnrehmeocntop  15634  cnplimcim  15691  limccnpcntop  15699  limccnp2lem  15700  limccnp2cntop  15701  dvfvalap  15705  dvidsslem  15717  dvmptfsum  15749  plyid  15770  logfac  15918  fsumdvdsmul  16019  gausslemma2dlem0b  16083  gausslemma2dlem0d  16085  gausslemma2dlem0h  16089  gausslemma2dlem5a  16098  gausslemma2dlem5  16099  gausslemma2dlem6  16100  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  2lgslem2  16125  2sqlem8  16156  struct2slots2dom  16193  structiedg0val  16195  edgstruct  16219  uhgrunop  16242  incistruhgr  16245  upgrunop  16282  umgrunop  16284  usgredg2v  16379  usgriedgdomord  16380  uspgredgdomord  16384  subgruhgredgdm  16425  uhgrspansubgrlem  16431  uhgrspanop  16437  upgrspanop  16438  umgrspanop  16439  usgrspanop  16440  vtxdgfval  16443  wksfval  16477  wlk1walkdom  16514  clwwlkg  16548  trlsegvdeglem3  16617  trlsegvdeglem5  16619  eupthvdres  16630  eupth2lem3fi  16631  eupth2lembfi  16632  bj-snexg  16852  trilpolemcl  16991