Theorem eqeltrrd 2309

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

Hypotheses

Ref	Expression
eqeltrrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqeltrrd.2	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Assertion

Ref	Expression
eqeltrrd	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Proof of Theorem eqeltrrd

Step	Hyp	Ref	Expression
1		eqeltrrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2237	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqeltrrd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2308	1 ⊢ (𝜑 → 𝐵 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

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

This theorem is referenced by:  3eltr3d  2314  exmid01  4288  pwntru  4289  xpexr2m  5178  funimaexg  5414  fvmptdv2  5736  ffvresb  5810  iotaexel  5976  2ndrn  6346  1st2ndbr  6347  elopabi  6360  cnvf1olem  6389  dftpos4  6429  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  nnmordi  6684  th3qlem1  6806  infiexmid  7066  onunsnss  7109  ssfirab  7129  ssfidc  7130  fnfi  7135  fidcenumlemr  7154  elfi2  7171  ordiso2  7234  djulclb  7254  ctmlemr  7307  ctssdccl  7310  ctssdc  7312  exmidfodomrlemreseldju  7411  exmidfodomrlemr  7413  pw1m  7442  exmidapne  7479  archnqq  7637  prarloclemarch2  7639  enq0tr  7654  nqnq0  7661  addcmpblnq0  7663  mulcmpblnq0  7664  mulcanenq0ec  7665  addclnq0  7671  mulclnq0  7672  nqpnq0nq  7673  nq0m0r  7676  distrnq0  7679  addassnq0lemcl  7681  prarloclemlt  7713  prarloclem5  7720  distrlem4prl  7804  distrlem4pru  7805  ltexprlemm  7820  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  cauappcvgprlemladdru  7876  prsrlem1  7962  mulgt0sr  7998  axpre-suploclemres  8121  cnegexlem2  8355  subf  8381  resubcl  8443  negcon1ad  8485  subeq0bd  8558  rimul  8765  rereim  8766  aprcl  8826  nn0nnaddcl  9433  elnn0nn  9444  zaddcllemneg  9518  zsubcl  9520  zrevaddcl  9530  elz2  9551  zdiv  9568  peano5uzti  9588  peano2uzr  9819  uzaddcl  9820  divfnzn  9855  qsubcl  9872  qrevaddcl  9878  fseq1p1m1  10329  suprzubdc  10497  modqmuladdim  10630  frec2uzrand  10668  frecuzrdglem  10674  frecuzrdg0  10676  frecuzrdgdomlem  10680  frecuzrdg0t  10685  frecuzrdgsuctlem  10686  seq3val  10723  seq3feq  10743  iseqf1olemnab  10764  seqf1oglem2  10783  seqfeq3  10792  seqfeq4g  10794  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  zesq  10921  bcm1k  11023  bccl  11030  permnn  11034  seq3coll  11107  ccatrn  11190  shftuz  11395  ref  11433  imf  11434  crre  11435  rereb  11441  resqrexlemnm  11596  absf  11688  summodclem2a  11960  summodc  11962  fsumgcl  11965  fsum3  11966  fsumf1o  11969  fsumcnv  12016  mptfzshft  12021  isumlessdc  12075  geolim2  12091  prodmodclem3  12154  fprodseq  12162  fprodf1o  12167  dvdsaddre2b  12420  3dvds  12443  oexpneg  12456  nn0ob  12487  divalglemqt  12498  gcdf  12561  lcmgcdlem  12667  sqnprm  12726  sqrt2irrlem  12751  2sqpwodd  12766  fnum  12780  fden  12781  phimullem  12815  pc2dvds  12921  gzsubcl  12971  4sqlem5  12973  4sqlem9  12977  4sqlem10  12978  mul4sqlem  12984  mul4sq  12985  4sqlem11  12992  4sqlem13m  12994  4sqlem16  12997  4sqlem17  12998  4sqlem18  12999  ctiunctlemfo  13078  ptex  13365  prdsval  13374  prdsbas  13377  prdsbascl  13390  mgmsscl  13462  subsubm  13584  mhmima  13592  imasgrp2  13715  mhmmnd  13721  mulgdir  13759  subgmulg  13793  issubg2m  13794  issubgrpd2  13795  grpissubg  13799  subsubg  13802  isnsg3  13812  ssnmz  13816  eqger  13829  eqgen  13832  ecqusaddcl  13844  ghmrn  13862  ghmnsgima  13873  conjsubg  13882  conjnmz  13884  ring1  14091  dvdsrvald  14126  dvdsrd  14127  dvdsrex  14131  0unit  14162  invrpropdg  14182  lringuplu  14229  subrngin  14246  subsubrng  14247  subrgcrng  14258  subrgin  14277  subsubrg  14278  islmodd  14326  lssvacl  14398  lssvancl1  14400  lss0cl  14402  lssvscl  14408  lssvnegcl  14409  lssincl  14418  issubrgd  14485  lidlrsppropdg  14528  2idlcpblrng  14556  zsssubrg  14618  unopn  14748  tsettps  14781  tgss2  14822  difopn  14851  resttop  14913  resttopon  14914  restco  14917  tgcn  14951  tgcnp  14952  cnptopco  14965  upxp  15015  txcn  15018  txdis  15020  cnmpt11  15026  cnmpt11f  15027  cnmpt1t  15028  cnmpt12  15030  cnmpt21  15034  cnmpt21f  15035  cnmpt2t  15036  cnmpt22  15037  cnmpt22f  15038  cnmpt1res  15039  xmeter  15179  mscl  15208  xmscl  15209  bdxmet  15244  cncfmpt1f  15341  cdivcncfap  15347  negfcncf  15349  ivthreinc  15388  cnmptlimc  15417  dvcnp2cntop  15442  elplyd  15484  plypow  15487  plyconst  15488  plyaddlem1  15490  plysub  15496  dvply2g  15509  sincn  15512  coscn  15513  relogcl  15605  mpodvdsmulf1o  15733  fsumdvdsmul  15734  mersenne  15740  perfect  15744  lgsne0  15786  lgseisenlem4  15821  lgsquadlem1  15825  usgr1vr  16118  p1evtxdeqfilem  16181  isclwwlkn  16283  clwwlknon  16299  pwtrufal  16649  qdiff  16704  gfsumcl  16739