Theorem eqeltrrd 2312

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eqeltrrd.1	|- ( ph -> A = B )
eqeltrrd.2	|- ( ph -> A e. C )

Assertion

Ref	Expression
eqeltrrd	|- ( ph -> B e. C )

Proof of Theorem eqeltrrd

Step	Hyp	Ref	Expression
1		eqeltrrd.1	. . 3 |- ( ph -> A = B )
2	1	eqcomd 2240	. 2 |- ( ph -> B = A )
3		eqeltrrd.2	. 2 |- ( ph -> A e. C )
4	2, 3	eqeltrd 2311	1 |- ( ph -> B e. C )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

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

This theorem is referenced by:  3eltr3d  2317  exmid01  4313  pwntru  4314  xpexr2m  5206  funimaexg  5442  fndmexd  5558  fvmptdv2  5769  ffvresb  5842  iotaexel  6010  2ndrn  6379  1st2ndbr  6380  elopabi  6393  cnvf1olem  6422  dftpos4  6496  tfrlemibxssdm  6560  tfr1onlembxssdm  6576  tfrcllembxssdm  6589  nnmordi  6751  th3qlem1  6873  infiexmid  7136  onunsnss  7179  ssfirab  7199  ssfidc  7200  fnfi  7205  fidcenumlemr  7227  elfi2  7261  ordiso2  7328  djulclb  7348  ctmlemr  7401  ctssdccl  7404  ctssdc  7406  exmidfodomrlemreseldju  7505  exmidfodomrlemr  7507  pw1m  7536  exmidapne  7576  archnqq  7734  prarloclemarch2  7736  enq0tr  7751  nqnq0  7758  addcmpblnq0  7760  mulcmpblnq0  7761  mulcanenq0ec  7762  addclnq0  7768  mulclnq0  7769  nqpnq0nq  7770  nq0m0r  7773  distrnq0  7776  addassnq0lemcl  7778  prarloclemlt  7810  prarloclem5  7817  distrlem4prl  7901  distrlem4pru  7902  ltexprlemm  7917  ltexprlemrl  7927  ltexprlemru  7929  addcanprleml  7931  cauappcvgprlemladdru  7973  prsrlem1  8059  mulgt0sr  8095  axpre-suploclemres  8218  cnegexlem2  8451  subf  8477  resubcl  8539  negcon1ad  8581  subeq0bd  8654  rimul  8861  rereim  8862  aprcl  8922  nn0nnaddcl  9529  elnn0nn  9540  zaddcllemneg  9618  zsubcl  9620  zrevaddcl  9630  elz2  9651  zdiv  9669  peano5uzti  9689  peano2uzr  9920  uzaddcl  9921  divfnzn  9956  qsubcl  9973  qrevaddcl  9979  fseq1p1m1  10432  suprzubdc  10600  modqmuladdim  10733  frec2uzrand  10771  frecuzrdglem  10777  frecuzrdg0  10779  frecuzrdgdomlem  10783  frecuzrdg0t  10788  frecuzrdgsuctlem  10789  seq3val  10826  seq3feq  10846  iseqf1olemnab  10867  seqf1oglem2  10886  seqfeq3  10895  seqfeq4g  10897  expaddzaplem  10948  expaddzap  10949  expmulzap  10951  zesq  11024  bcm1k  11126  bccl  11133  permnn  11138  seq3coll  11218  ccatrn  11301  shftuz  11506  ref  11544  imf  11545  crre  11546  rereb  11552  resqrexlemnm  11707  absf  11799  summodclem2a  12071  summodc  12073  fsumgcl  12076  fsum3  12077  fsumf1o  12080  fsumcnv  12127  mptfzshft  12132  isumlessdc  12186  geolim2  12202  prodmodclem3  12265  fprodseq  12273  fprodf1o  12278  dvdsaddre2b  12531  3dvds  12554  oexpneg  12567  nn0ob  12598  divalglemqt  12609  gcdf  12672  lcmgcdlem  12778  sqnprm  12837  sqrt2irrlem  12862  2sqpwodd  12877  fnum  12891  fden  12892  phimullem  12926  pc2dvds  13032  gzsubcl  13082  4sqlem5  13084  4sqlem9  13088  4sqlem10  13089  mul4sqlem  13095  mul4sq  13096  4sqlem11  13103  4sqlem13m  13105  4sqlem16  13108  4sqlem17  13109  4sqlem18  13110  ballotfilem2  13149  ctiunctlemfo  13207  ptex  13494  prdsval  13503  prdsbas  13506  prdsbascl  13519  mgmsscl  13591  subsubm  13713  mhmima  13721  imasgrp2  13844  mhmmnd  13850  mulgdir  13888  subgmulg  13922  issubg2m  13923  issubgrpd2  13924  grpissubg  13928  subsubg  13931  isnsg3  13941  ssnmz  13945  eqger  13958  eqgen  13961  ecqusaddcl  13973  ghmrn  13991  ghmnsgima  14002  conjsubg  14011  conjnmz  14013  ring1  14220  dvdsrvald  14255  dvdsrd  14256  dvdsrex  14260  0unit  14291  invrpropdg  14311  lringuplu  14358  subrngin  14375  subsubrng  14376  subrgcrng  14387  subrgin  14406  subsubrg  14407  aprnzr  14450  aprlring  14451  islmodd  14458  lssvacl  14530  lssvancl1  14532  lss0cl  14534  lssvscl  14540  lssvnegcl  14541  lssincl  14550  issubrgd  14617  lidlrsppropdg  14660  2idlcpblrng  14688  zsssubrg  14750  unopn  14887  tsettps  14920  tgss2  14961  difopn  14990  resttop  15052  resttopon  15053  restco  15056  tgcn  15090  tgcnp  15091  cnptopco  15104  upxp  15154  txcn  15157  txdis  15159  cnmpt11  15165  cnmpt11f  15166  cnmpt1t  15167  cnmpt12  15169  cnmpt21  15173  cnmpt21f  15174  cnmpt2t  15175  cnmpt22  15176  cnmpt22f  15177  cnmpt1res  15178  xmeter  15318  mscl  15347  xmscl  15348  bdxmet  15383  cncfmpt1f  15480  cdivcncfap  15486  negfcncf  15488  ivthreinc  15527  cnmptlimc  15556  dvcnp2cntop  15581  elplyd  15623  plypow  15626  plyconst  15627  plyaddlem1  15629  plysub  15635  dvply2g  15648  sincn  15651  coscn  15652  relogcl  15744  mpodvdsmulf1o  15875  fsumdvdsmul  15876  mersenne  15882  perfect  15886  lgsne0  15928  lgseisenlem4  15963  lgsquadlem1  15967  usgr1vr  16260  p1evtxdeqfilem  16323  isclwwlkn  16425  clwwlknon  16441  pwtrufal  16788  repiecele0  16827  qdiff  16850  gfsumcl  16887