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  6539  tfrlemibxssdm  6603  tfr1onlembxssdm  6619  tfrcllembxssdm  6632  nnmordi  6794  th3qlem1  6916  infiexmid  7187  onunsnss  7230  ssfirab  7250  ssfidc  7251  fnfi  7256  fidcenumlemr  7279  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  9692  zsubcl  9694  zrevaddcl  9704  elz2  9725  zdiv  9744  peano5uzti  9764  peano2uzr  10000  uzaddcl  10001  divfnzn  10036  qsubcl  10053  qrevaddcl  10059  fseq1p1m1  10517  suprzubdc  10687  modqmuladdim  10824  frec2uzrand  10862  frecuzrdglem  10868  frecuzrdg0  10870  frecuzrdgdomlem  10874  frecuzrdg0t  10879  frecuzrdgsuctlem  10880  seq3val  10917  seq3feq  10937  iseqf1olemnab  10958  seqf1oglem2  10977  seqfeq3  10986  seqfeq4g  10988  expaddzaplem  11039  expaddzap  11040  expmulzap  11042  zesq  11116  bcm1k  11219  bccl  11226  permnn  11231  hashf1lem2  11307  hashf1  11308  seq3coll  11315  ccatrn  11398  shftuz  11603  ref  11641  imf  11642  crre  11643  rereb  11649  resqrexlemnm  11805  absf  11898  summodclem2a  12172  summodc  12174  fsumgcl  12177  fsum3  12178  fsumf1o  12181  fsumcnv  12228  mptfzshft  12233  isumlessdc  12287  geolim2  12303  prodmodclem3  12366  fprodseq  12374  fprodf1o  12379  dvdsaddre2b  12632  3dvds  12655  oexpneg  12668  nn0ob  12699  divalglemqt  12710  gcdf  12773  lcmgcdlem  12879  sqnprm  12939  sqrt2irrlem  12964  2sqpwodd  12980  fnum  12994  fden  12995  nn0sqdcq  13012  phimullem  13031  pc2dvds  13137  gzsubcl  13187  4sqlem5  13189  4sqlem9  13193  4sqlem10  13194  mul4sqlem  13200  mul4sq  13201  4sqlem11  13208  4sqlem13m  13210  4sqlem16  13213  4sqlem17  13214  4sqlem18  13215  ballotfilem2  13285  ballotfilemsf1o  13314  ballotfilemrinv0  13333  ctiunctlemfo  13387  ptex  13676  mgmsscl  13739  subsubm  13848  mhmima  13856  imasgrp2  13971  mhmmnd  13977  mulgdir  14015  subgmulg  14049  issubg2m  14050  issubgrpd2  14051  grpissubg  14055  subsubg  14058  isnsg3  14068  ssnmz  14072  eqger  14085  eqgen  14088  ecqusaddcl  14100  ghmrn  14118  ghmnsgima  14129  conjsubg  14138  conjnmz  14140  gsumclfi  14248  gsumsubmclfi  14252  prdsval  14279  prdsbas  14282  prdsbascl  14295  ring1  14470  dvdsrvald  14508  dvdsrd  14509  dvdsrex  14513  0unit  14544  invrpropdg  14564  lringuplu  14611  subrngin  14629  subsubrng  14630  subrgcrng  14641  subrgin  14660  subsubrg  14661  aprnzr  14707  aprlring  14708  islmodd  14737  lssvacl  14810  lssvancl1  14812  lss0cl  14814  lssvscl  14820  lssvnegcl  14821  lssincl  14830  issubrgd  14897  lidlrsppropdg  14940  2idlcpblrng  14968  zsssubrg  15030  issubassa2  15143  psrbaglefifi  15175  psrbagmaxlemfi  15180  psrass1filem  15186  unopn  15248  tsettps  15281  tgss2  15322  difopn  15351  resttop  15413  resttopon  15414  restco  15417  tgcn  15451  tgcnp  15452  cnptopco  15465  upxp  15515  txcn  15518  txdis  15520  cnmpt11  15526  cnmpt11f  15527  cnmpt1t  15528  cnmpt12  15530  cnmpt21  15534  cnmpt21f  15535  cnmpt2t  15536  cnmpt22  15537  cnmpt22f  15538  cnmpt1res  15539  xmeter  15679  mscl  15708  xmscl  15709  bdxmet  15744  cncfmpt1f  15841  cdivcncfap  15847  negfcncf  15849  ivthreinc  15888  cnmptlimc  15917  dvcnp2cntop  15942  elplyd  15984  plypow  15987  plyconst  15988  plyaddlem1  15990  plysub  15996  dvply2g  16009  sincn  16012  coscn  16013  relogcl  16108  ppiprm  16276  ppinprm  16277  chtprm  16278  chtnprm  16279  efchtqdvds  16282  prmorcht  16299  mpodvdsmulf1o  16301  fsumdvdsmul  16302  chtublem  16312  mersenne  16314  perfect  16318  lgsne0  16379  lgseisenlem4  16414  lgsquadlem1  16418  usgr1vr  16711  p1evtxdeqfilem  16774  isclwwlkn  16876  clwwlknon  16892  pwtrufal  17249  repiecele0  17298  qdiff  17322