Theorem eqeltrrd 2316

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 2244	. 2 |- ( ph -> B = A )
3		eqeltrrd.2	. 2 |- ( ph -> A e. C )
4	2, 3	eqeltrd 2315	1 |- ( ph -> B 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:  3eltr3d  2321  exmid01  4337  pwntru  4338  xpexr2m  5232  funimaexg  5468  fndmexd  5584  fvmptdv2  5798  ffvresb  5874  iotaexel  6046  2ndrn  6421  1st2ndbr  6422  elopabi  6435  cnvf1olem  6464  dftpos4  6538  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  nnmordi  6793  th3qlem1  6915  infiexmid  7185  onunsnss  7228  ssfirab  7248  ssfidc  7249  fnfi  7254  fidcenumlemr  7277  elfi2  7311  f1setfi  7322  ordiso2  7381  djulclb  7401  ctmlemr  7454  ctssdccl  7457  ctssdc  7459  exmidfodomrlemreseldju  7558  exmidfodomrlemr  7560  pw1m  7589  exmidapne  7632  archnqq  7790  prarloclemarch2  7792  enq0tr  7807  nqnq0  7814  addcmpblnq0  7816  mulcmpblnq0  7817  mulcanenq0ec  7818  addclnq0  7824  mulclnq0  7825  nqpnq0nq  7826  nq0m0r  7829  distrnq0  7832  addassnq0lemcl  7834  prarloclemlt  7866  prarloclem5  7873  distrlem4prl  7957  distrlem4pru  7958  ltexprlemm  7973  ltexprlemrl  7983  ltexprlemru  7985  addcanprleml  7987  cauappcvgprlemladdru  8029  prsrlem1  8115  mulgt0sr  8151  axpre-suploclemres  8274  cnegexlem2  8509  subf  8535  resubcl  8597  negcon1ad  8639  subeq0bd  8713  rimul  8921  rereim  8922  aprcl  8982  nn0nnaddcl  9605  elnn0nn  9616  zaddcllemneg  9694  zsubcl  9696  zrevaddcl  9706  elz2  9727  zdiv  9745  peano5uzti  9765  peano2uzr  10001  uzaddcl  10002  divfnzn  10037  qsubcl  10054  qrevaddcl  10060  fseq1p1m1  10518  suprzubdc  10688  modqmuladdim  10825  frec2uzrand  10863  frecuzrdglem  10869  frecuzrdg0  10871  frecuzrdgdomlem  10875  frecuzrdg0t  10880  frecuzrdgsuctlem  10881  seq3val  10918  seq3feq  10938  iseqf1olemnab  10959  seqf1oglem2  10978  seqfeq3  10987  seqfeq4g  10989  expaddzaplem  11040  expaddzap  11041  expmulzap  11043  zesq  11117  bcm1k  11220  bccl  11227  permnn  11232  hashf1lem2  11308  hashf1  11309  seq3coll  11316  ccatrn  11399  shftuz  11604  ref  11642  imf  11643  crre  11644  rereb  11650  resqrexlemnm  11806  absf  11899  summodclem2a  12173  summodc  12175  fsumgcl  12178  fsum3  12179  fsumf1o  12182  fsumcnv  12229  mptfzshft  12234  isumlessdc  12288  geolim2  12304  prodmodclem3  12367  fprodseq  12375  fprodf1o  12380  dvdsaddre2b  12633  3dvds  12656  oexpneg  12669  nn0ob  12700  divalglemqt  12711  gcdf  12774  lcmgcdlem  12880  sqnprm  12940  sqrt2irrlem  12965  2sqpwodd  12981  fnum  12995  fden  12996  nn0sqdcq  13013  phimullem  13032  pc2dvds  13138  gzsubcl  13188  4sqlem5  13190  4sqlem9  13194  4sqlem10  13195  mul4sqlem  13201  mul4sq  13202  4sqlem11  13209  4sqlem13m  13211  4sqlem16  13214  4sqlem17  13215  4sqlem18  13216  ballotfilem2  13286  ballotfilemsf1o  13315  ballotfilemrinv0  13334  ctiunctlemfo  13388  ptex  13677  mgmsscl  13740  subsubm  13849  mhmima  13857  imasgrp2  13972  mhmmnd  13978  mulgdir  14016  subgmulg  14050  issubg2m  14051  issubgrpd2  14052  grpissubg  14056  subsubg  14059  isnsg3  14069  ssnmz  14073  eqger  14086  eqgen  14089  ecqusaddcl  14101  ghmrn  14119  ghmnsgima  14130  conjsubg  14139  conjnmz  14141  gsumclfi  14249  gsumsubmclfi  14253  prdsval  14280  prdsbas  14283  prdsbascl  14296  ring1  14471  dvdsrvald  14509  dvdsrd  14510  dvdsrex  14514  0unit  14545  invrpropdg  14565  lringuplu  14612  subrngin  14630  subsubrng  14631  subrgcrng  14642  subrgin  14661  subsubrg  14662  aprnzr  14708  aprlring  14709  islmodd  14738  lssvacl  14811  lssvancl1  14813  lss0cl  14815  lssvscl  14821  lssvnegcl  14822  lssincl  14831  issubrgd  14898  lidlrsppropdg  14941  2idlcpblrng  14969  zsssubrg  15031  issubassa2  15144  psrbaglefifi  15172  psrass1filem  15177  unopn  15231  tsettps  15264  tgss2  15305  difopn  15334  resttop  15396  resttopon  15397  restco  15400  tgcn  15434  tgcnp  15435  cnptopco  15448  upxp  15498  txcn  15501  txdis  15503  cnmpt11  15509  cnmpt11f  15510  cnmpt1t  15511  cnmpt12  15513  cnmpt21  15517  cnmpt21f  15518  cnmpt2t  15519  cnmpt22  15520  cnmpt22f  15521  cnmpt1res  15522  xmeter  15662  mscl  15691  xmscl  15692  bdxmet  15727  cncfmpt1f  15824  cdivcncfap  15830  negfcncf  15832  ivthreinc  15871  cnmptlimc  15900  dvcnp2cntop  15925  elplyd  15967  plypow  15970  plyconst  15971  plyaddlem1  15973  plysub  15979  dvply2g  15992  sincn  15995  coscn  15996  relogcl  16091  ppiprm  16259  ppinprm  16260  chtprm  16261  chtnprm  16262  efchtqdvds  16265  prmorcht  16282  mpodvdsmulf1o  16284  fsumdvdsmul  16285  chtublem  16295  mersenne  16297  perfect  16301  lgsne0  16362  lgseisenlem4  16397  lgsquadlem1  16401  usgr1vr  16694  p1evtxdeqfilem  16757  isclwwlkn  16859  clwwlknon  16875  pwtrufal  17232  repiecele0  17281  qdiff  17305