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  8526  intqfrac2  10756  intfracq  10757  frec2uzzd  10837  frecuzrdgrrn  10845  iseqf1olemqpcl  10946  seq3f1olemqsum  10950  seqf1oglem1  10956  seqf1oglem2  10957  bcval5  11201  hashf1lem2  11286  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12  11505  pfxccat3  11506  pfxccatpfx2  11509  pfxccat3a  11510  swrdccat3blem  11511  swrdccat3b  11512  cats1cld  11535  xrmaxiflemval  12016  climmpt  12066  reccn2ap  12079  zsumdc  12151  fsumzcl2  12172  fsump1i  12200  fsumabs  12232  hash2iun1dif1  12247  mertenslemi1  12302  fprodcllemf  12380  bitsfzolem  12721  nninfctlemfo  12817  algrf  12823  algcvg  12826  algcvga  12829  algfx  12830  eucalgcvga  12836  eucalg  12837  crth  13002  phimullem  13003  eulerthlemth  13010  prmdiv  13013  pythagtriplem11  13053  pythagtriplem13  13055  pcprecl  13068  infpnlem1  13138  infpnlem2  13139  4sqlem5  13161  mul4sqlem  13172  4sqlemafi  13174  4sqlem13m  13182  4sqlem14  13183  4sqlem17  13186  4sqlem18  13187  ennnfonelemj0  13292  ennnfonelemom  13299  ressbasid  13424  ressval3d  13426  1strbas  13471  2strbasg  13474  2stropg  13475  restid  13604  topnvalg  13605  topnidg  13606  imasival  13627  imasmulr  13630  imasaddfn  13638  imasaddval  13639  imasaddf  13640  imasmulfn  13641  imasmulval  13642  imasmulf  13643  qusval  13644  qusaddval  13656  qusaddf  13657  qusmulval  13658  qusmulf  13659  plusffvalg  13682  plusfvalg  13683  grpidvalg  13693  gzsumvalx  13709  gzsumfzval  13711  gzsum0  13713  gzsumsplit1r  13715  issubmnd  13755  ress0g  13756  ismhm  13768  0mhm  13793  grpinvfvalg  13847  grpinvval  13848  grpinvfng  13849  grpsubfvalg  13850  grpsubval  13851  grpressid  13866  grplactfval  13906  mulgfvalg  13924  mulgval  13925  mulgfng  13927  mulgnngzsum  13930  mulgnnp1  13933  mulgnndir  13954  issubg  13976  subggrp  13980  issubg2m  13992  eqgfval  14025  eqgen  14030  quselbasg  14033  quseccl0g  14034  isghm  14046  ghmima  14068  ablressid  14139  gzsumshift  14149  gsumclfi  14159  gsumsubmclfi  14163  prdsval  14173  prdsplusg  14177  prdsmulr  14178  prdssgrpd  14191  prdsinvlem  14196  xpsval  14201  pwsval  14204  pwselbasb  14206  pwssnf1o  14211  mgpvalg  14220  mgpplusgg  14221  mgptopng  14228  mgpress  14230  rngressid  14253  issrg  14269  ringidss  14334  ring1  14364  ringressid  14368  opprvalg  14374  opprmulfvalg  14375  rdivmuldivd  14451  isnzr2  14491  issubrg  14529  subrgring  14532  rrgval  14570  islmod  14627  scaffvalg  14643  scafvalg  14644  lsssetm  14693  islssm  14694  islssmg  14695  lss1d  14720  lspfval  14725  lspval  14727  lspcl  14728  ellspsn  14754  rnglidlmmgm  14833  rnglidlmsgrp  14834  2idlval  14839  2idlvalg  14840  qusrhm  14865  zlmval  14962  zlmvscag  14968  znval  14971  znle  14972  znbaslemnn  14974  znbas  14979  znzrhval  14982  znleval  14988  aspval  15015  asclfval  15021  psrval  15050  psrbasg  15065  psrelbas  15066  psrplusgg  15069  mplvalcoe  15081  mplbascoe  15082  mplplusgg  15094  topopn  15109  topcld  15210  uncld  15214  iuncld  15216  unicld  15217  tgrest  15270  restin  15277  cnco  15322  cnrest  15336  cnptoprest2  15341  lmss  15347  txbasval  15368  txcn  15376  cnmpt12f  15387  hmeoco  15417  idhmeo  15418  blres  15535  metrest  15607  qtopbasss  15622  tgqioo  15656  divcnap  15666  fsumcncntop  15668  cncfmet  15693  sub1cncf  15703  sub2cncf  15704  cdivcncfap  15705  cnrehmeocntop  15711  cnplimcim  15768  limccnpcntop  15776  limccnp2lem  15777  limccnp2cntop  15778  dvfvalap  15782  dvidsslem  15794  dvmptfsum  15826  plyid  15847  logfac  15995  fsumdvdsmul  16105  gausslemma2dlem0b  16169  gausslemma2dlem0d  16171  gausslemma2dlem0h  16175  gausslemma2dlem5a  16184  gausslemma2dlem5  16185  gausslemma2dlem6  16186  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  2lgslem2  16211  2sqlem8  16242  struct2slots2dom  16279  structiedg0val  16281  edgstruct  16305  uhgrunop  16328  incistruhgr  16331  upgrunop  16368  umgrunop  16370  usgredg2v  16465  usgriedgdomord  16466  uspgredgdomord  16470  subgruhgredgdm  16511  uhgrspansubgrlem  16517  uhgrspanop  16523  upgrspanop  16524  umgrspanop  16525  usgrspanop  16526  vtxdgfval  16529  wksfval  16563  wlk1walkdom  16600  clwwlkg  16634  trlsegvdeglem3  16703  trlsegvdeglem5  16705  eupthvdres  16716  eupth2lem3fi  16717  eupth2lembfi  16718  bj-snexg  16938  trilpolemcl  17086