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 )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eqeltrrid  2326  csbexga  4261  rabexd  4281  otexg  4370  tpexg  4590  dmresexg  5086  f1oabexg  5651  funfvex  5712  elfvfvex  5730  riotaexg  6042  riotaeqimp  6063  riotaprop  6064  fnovex  6118  ovexg  6119  elovimad  6129  fovcdm  6232  fnovrn  6237  cofunexg  6338  cofunex2g  6339  abrexex2g  6349  xpexgALT  6366  mpofvex  6441  mptsuppdifd  6495  tfrex  6639  frec0g  6668  freccllem  6673  ecexg  6811  qsexg  6865  pmex  6927  elixpsn  7017  diffifi  7198  unfidisj  7229  prfidisj  7234  tpfidisj  7236  tpfidceq  7237  ssfirab  7244  ssfidc  7245  fnfi  7250  funrnfi  7256  iunfidisj  7260  infclti  7363  supex2g  7373  infex2g  7374  djuex  7383  ctssdccl  7451  addvalex  8211  negcl  8527  intqfrac2  10769  intfracq  10770  frec2uzzd  10850  frecuzrdgrrn  10858  iseqf1olemqpcl  10959  seq3f1olemqsum  10963  seqf1oglem1  10969  seqf1oglem2  10970  bcval5  11215  hashf1lem2  11300  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12  11519  pfxccat3  11520  pfxccatpfx2  11523  pfxccat3a  11524  swrdccat3blem  11525  swrdccat3b  11526  cats1cld  11549  xrmaxiflemval  12032  climmpt  12082  reccn2ap  12095  zsumdc  12167  fsumzcl2  12188  fsump1i  12216  fsumabs  12248  hash2iun1dif1  12263  mertenslemi1  12318  fprodcllemf  12396  bitsfzolem  12737  nninfctlemfo  12833  algrf  12839  algcvg  12842  algcvga  12845  algfx  12846  eucalgcvga  12852  eucalg  12853  crth  13022  phimullem  13023  eulerthlemth  13030  prmdiv  13033  pythagtriplem11  13073  pythagtriplem13  13075  pcprecl  13088  infpnlem1  13158  infpnlem2  13159  4sqlem5  13181  mul4sqlem  13192  4sqlemafi  13194  4sqlem13m  13202  4sqlem14  13203  4sqlem17  13206  4sqlem18  13207  ennnfonelemj0  13341  ennnfonelemom  13348  ressbasid  13473  ressval3d  13475  1strbas  13520  2strbasg  13523  2stropg  13524  restid  13653  topnvalg  13654  topnidg  13655  imasival  13676  imasmulr  13679  imasaddfn  13687  imasaddval  13688  imasaddf  13689  imasmulfn  13690  imasmulval  13691  imasmulf  13692  qusval  13693  qusaddval  13705  qusaddf  13706  qusmulval  13707  qusmulf  13708  plusffvalg  13731  plusfvalg  13732  grpidvalg  13742  gzsumvalx  13758  gzsumfzval  13760  gzsum0  13762  gzsumsplit1r  13764  issubmnd  13804  ress0g  13805  ismhm  13817  0mhm  13842  grpinvfvalg  13896  grpinvval  13897  grpinvfng  13898  grpsubfvalg  13899  grpsubval  13900  grpressid  13915  grplactfval  13955  mulgfvalg  13973  mulgval  13974  mulgfng  13976  mulgnngzsum  13979  mulgnnp1  13982  mulgnndir  14003  issubg  14025  subggrp  14029  issubg2m  14041  eqgfval  14074  eqgen  14079  quselbasg  14082  quseccl0g  14083  isghm  14095  ghmima  14117  ablressid  14188  gzsumshift  14198  gsumclfi  14208  gsumsubmclfi  14212  prdsval  14222  prdsplusg  14226  prdsmulr  14227  prdssgrpd  14240  prdsinvlem  14245  xpsval  14250  pwsval  14253  pwselbasb  14255  pwssnf1o  14260  mgpvalg  14269  mgpplusgg  14270  mgptopng  14277  mgpress  14279  rngressid  14302  issrg  14318  ringidss  14383  ring1  14413  ringressid  14417  opprvalg  14423  opprmulfvalg  14424  rdivmuldivd  14500  isnzr2  14540  issubrg  14578  subrgring  14581  rrgval  14619  islmod  14676  scaffvalg  14692  scafvalg  14693  lsssetm  14742  islssm  14743  islssmg  14744  lss1d  14769  lspfval  14774  lspval  14776  lspcl  14777  ellspsn  14803  rnglidlmmgm  14882  rnglidlmsgrp  14883  2idlval  14888  2idlvalg  14889  qusrhm  14914  zlmval  15011  zlmvscag  15017  znval  15020  znle  15021  znbaslemnn  15023  znbas  15028  znzrhval  15031  znleval  15037  aspval  15064  asclfval  15070  psrval  15099  psrbasg  15114  psrelbas  15115  psrplusgg  15118  mplvalcoe  15130  mplbascoe  15131  mplplusgg  15143  topopn  15158  topcld  15259  uncld  15263  iuncld  15265  unicld  15266  tgrest  15319  restin  15326  cnco  15371  cnrest  15385  cnptoprest2  15390  lmss  15396  txbasval  15417  txcn  15425  cnmpt12f  15436  hmeoco  15466  idhmeo  15467  blres  15584  metrest  15656  qtopbasss  15671  tgqioo  15705  divcnap  15715  fsumcncntop  15717  cncfmet  15742  sub1cncf  15752  sub2cncf  15753  cdivcncfap  15754  cnrehmeocntop  15760  cnplimcim  15817  limccnpcntop  15825  limccnp2lem  15826  limccnp2cntop  15827  dvfvalap  15831  dvidsslem  15843  dvmptfsum  15875  plyid  15896  logfac  16048  fsumdvdsmul  16186  bposlem3  16211  bposlem5  16213  gausslemma2dlem0b  16267  gausslemma2dlem0d  16269  gausslemma2dlem0h  16273  gausslemma2dlem5a  16282  gausslemma2dlem5  16283  gausslemma2dlem6  16284  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  2lgslem2  16309  2sqlem8  16340  struct2slots2dom  16377  structiedg0val  16379  edgstruct  16403  uhgrunop  16426  incistruhgr  16429  upgrunop  16466  umgrunop  16468  usgredg2v  16563  usgriedgdomord  16564  uspgredgdomord  16568  subgruhgredgdm  16609  uhgrspansubgrlem  16615  uhgrspanop  16621  upgrspanop  16622  umgrspanop  16623  usgrspanop  16624  vtxdgfval  16627  wksfval  16661  wlk1walkdom  16698  clwwlkg  16732  trlsegvdeglem3  16801  trlsegvdeglem5  16803  eupthvdres  16814  eupth2lem3fi  16815  eupth2lembfi  16816  bj-snexg  17036  trilpolemcl  17184