Theorem eqeltrrd 2307

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 2235	. 2 |- ( ph -> B = A )
3		eqeltrrd.2	. 2 |- ( ph -> A e. C )
4	2, 3	eqeltrd 2306	1 |- ( ph -> B e. C )

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  3eltr3d  2312  exmid01  4283  pwntru  4284  xpexr2m  5173  funimaexg  5408  fvmptdv2  5729  ffvresb  5803  iotaexel  5968  2ndrn  6338  1st2ndbr  6339  elopabi  6352  cnvf1olem  6381  dftpos4  6420  tfrlemibxssdm  6484  tfr1onlembxssdm  6500  tfrcllembxssdm  6513  nnmordi  6675  th3qlem1  6797  infiexmid  7052  onunsnss  7095  ssfirab  7114  ssfidc  7115  fnfi  7119  fidcenumlemr  7138  elfi2  7155  ordiso2  7218  djulclb  7238  ctmlemr  7291  ctssdccl  7294  ctssdc  7296  exmidfodomrlemreseldju  7394  exmidfodomrlemr  7396  pw1m  7425  exmidapne  7462  archnqq  7620  prarloclemarch2  7622  enq0tr  7637  nqnq0  7644  addcmpblnq0  7646  mulcmpblnq0  7647  mulcanenq0ec  7648  addclnq0  7654  mulclnq0  7655  nqpnq0nq  7656  nq0m0r  7659  distrnq0  7662  addassnq0lemcl  7664  prarloclemlt  7696  prarloclem5  7703  distrlem4prl  7787  distrlem4pru  7788  ltexprlemm  7803  ltexprlemrl  7813  ltexprlemru  7815  addcanprleml  7817  cauappcvgprlemladdru  7859  prsrlem1  7945  mulgt0sr  7981  axpre-suploclemres  8104  cnegexlem2  8338  subf  8364  resubcl  8426  negcon1ad  8468  subeq0bd  8541  rimul  8748  rereim  8749  aprcl  8809  nn0nnaddcl  9416  elnn0nn  9427  zaddcllemneg  9501  zsubcl  9503  zrevaddcl  9513  elz2  9534  zdiv  9551  peano5uzti  9571  peano2uzr  9797  uzaddcl  9798  divfnzn  9833  qsubcl  9850  qrevaddcl  9856  fseq1p1m1  10307  suprzubdc  10473  modqmuladdim  10606  frec2uzrand  10644  frecuzrdglem  10650  frecuzrdg0  10652  frecuzrdgdomlem  10656  frecuzrdg0t  10661  frecuzrdgsuctlem  10662  seq3val  10699  seq3feq  10719  iseqf1olemnab  10740  seqf1oglem2  10759  seqfeq3  10768  seqfeq4g  10770  expaddzaplem  10821  expaddzap  10822  expmulzap  10824  zesq  10897  bcm1k  10999  bccl  11006  permnn  11010  seq3coll  11082  ccatrn  11162  shftuz  11349  ref  11387  imf  11388  crre  11389  rereb  11395  resqrexlemnm  11550  absf  11642  summodclem2a  11913  summodc  11915  fsumgcl  11918  fsum3  11919  fsumf1o  11922  fsumcnv  11969  mptfzshft  11974  isumlessdc  12028  geolim2  12044  prodmodclem3  12107  fprodseq  12115  fprodf1o  12120  dvdsaddre2b  12373  3dvds  12396  oexpneg  12409  nn0ob  12440  divalglemqt  12451  gcdf  12514  lcmgcdlem  12620  sqnprm  12679  sqrt2irrlem  12704  2sqpwodd  12719  fnum  12733  fden  12734  phimullem  12768  pc2dvds  12874  gzsubcl  12924  4sqlem5  12926  4sqlem9  12930  4sqlem10  12931  mul4sqlem  12937  mul4sq  12938  4sqlem11  12945  4sqlem13m  12947  4sqlem16  12950  4sqlem17  12951  4sqlem18  12952  ctiunctlemfo  13031  ptex  13318  prdsval  13327  prdsbas  13330  prdsbascl  13343  mgmsscl  13415  subsubm  13537  mhmima  13545  imasgrp2  13668  mhmmnd  13674  mulgdir  13712  subgmulg  13746  issubg2m  13747  issubgrpd2  13748  grpissubg  13752  subsubg  13755  isnsg3  13765  ssnmz  13769  eqger  13782  eqgen  13785  ecqusaddcl  13797  ghmrn  13815  ghmnsgima  13826  conjsubg  13835  conjnmz  13837  ring1  14043  dvdsrvald  14078  dvdsrd  14079  dvdsrex  14083  0unit  14114  invrpropdg  14134  lringuplu  14181  subrngin  14198  subsubrng  14199  subrgcrng  14210  subrgin  14229  subsubrg  14230  islmodd  14278  lssvacl  14350  lssvancl1  14352  lss0cl  14354  lssvscl  14360  lssvnegcl  14361  lssincl  14370  issubrgd  14437  lidlrsppropdg  14480  2idlcpblrng  14508  zsssubrg  14570  unopn  14700  tsettps  14733  tgss2  14774  difopn  14803  resttop  14865  resttopon  14866  restco  14869  tgcn  14903  tgcnp  14904  cnptopco  14917  upxp  14967  txcn  14970  txdis  14972  cnmpt11  14978  cnmpt11f  14979  cnmpt1t  14980  cnmpt12  14982  cnmpt21  14986  cnmpt21f  14987  cnmpt2t  14988  cnmpt22  14989  cnmpt22f  14990  cnmpt1res  14991  xmeter  15131  mscl  15160  xmscl  15161  bdxmet  15196  cncfmpt1f  15293  cdivcncfap  15299  negfcncf  15301  ivthreinc  15340  cnmptlimc  15369  dvcnp2cntop  15394  elplyd  15436  plypow  15439  plyconst  15440  plyaddlem1  15442  plysub  15448  dvply2g  15461  sincn  15464  coscn  15465  relogcl  15557  mpodvdsmulf1o  15685  fsumdvdsmul  15686  mersenne  15692  perfect  15696  lgsne0  15738  lgseisenlem4  15773  lgsquadlem1  15777  usgr1vr  16067  pwtrufal  16476