Theorem eqeltrrd 2307

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 2235	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqeltrrd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2306	1 ⊢ (𝜑 → 𝐵 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1395   ∈ 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  4286  pwntru  4287  xpexr2m  5176  funimaexg  5411  fvmptdv2  5732  ffvresb  5806  iotaexel  5971  2ndrn  6341  1st2ndbr  6342  elopabi  6355  cnvf1olem  6384  dftpos4  6424  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  nnmordi  6679  th3qlem1  6801  infiexmid  7059  onunsnss  7102  ssfirab  7121  ssfidc  7122  fnfi  7126  fidcenumlemr  7145  elfi2  7162  ordiso2  7225  djulclb  7245  ctmlemr  7298  ctssdccl  7301  ctssdc  7303  exmidfodomrlemreseldju  7401  exmidfodomrlemr  7403  pw1m  7432  exmidapne  7469  archnqq  7627  prarloclemarch2  7629  enq0tr  7644  nqnq0  7651  addcmpblnq0  7653  mulcmpblnq0  7654  mulcanenq0ec  7655  addclnq0  7661  mulclnq0  7662  nqpnq0nq  7663  nq0m0r  7666  distrnq0  7669  addassnq0lemcl  7671  prarloclemlt  7703  prarloclem5  7710  distrlem4prl  7794  distrlem4pru  7795  ltexprlemm  7810  ltexprlemrl  7820  ltexprlemru  7822  addcanprleml  7824  cauappcvgprlemladdru  7866  prsrlem1  7952  mulgt0sr  7988  axpre-suploclemres  8111  cnegexlem2  8345  subf  8371  resubcl  8433  negcon1ad  8475  subeq0bd  8548  rimul  8755  rereim  8756  aprcl  8816  nn0nnaddcl  9423  elnn0nn  9434  zaddcllemneg  9508  zsubcl  9510  zrevaddcl  9520  elz2  9541  zdiv  9558  peano5uzti  9578  peano2uzr  9809  uzaddcl  9810  divfnzn  9845  qsubcl  9862  qrevaddcl  9868  fseq1p1m1  10319  suprzubdc  10486  modqmuladdim  10619  frec2uzrand  10657  frecuzrdglem  10663  frecuzrdg0  10665  frecuzrdgdomlem  10669  frecuzrdg0t  10674  frecuzrdgsuctlem  10675  seq3val  10712  seq3feq  10732  iseqf1olemnab  10753  seqf1oglem2  10772  seqfeq3  10781  seqfeq4g  10783  expaddzaplem  10834  expaddzap  10835  expmulzap  10837  zesq  10910  bcm1k  11012  bccl  11019  permnn  11023  seq3coll  11096  ccatrn  11176  shftuz  11368  ref  11406  imf  11407  crre  11408  rereb  11414  resqrexlemnm  11569  absf  11661  summodclem2a  11932  summodc  11934  fsumgcl  11937  fsum3  11938  fsumf1o  11941  fsumcnv  11988  mptfzshft  11993  isumlessdc  12047  geolim2  12063  prodmodclem3  12126  fprodseq  12134  fprodf1o  12139  dvdsaddre2b  12392  3dvds  12415  oexpneg  12428  nn0ob  12459  divalglemqt  12470  gcdf  12533  lcmgcdlem  12639  sqnprm  12698  sqrt2irrlem  12723  2sqpwodd  12738  fnum  12752  fden  12753  phimullem  12787  pc2dvds  12893  gzsubcl  12943  4sqlem5  12945  4sqlem9  12949  4sqlem10  12950  mul4sqlem  12956  mul4sq  12957  4sqlem11  12964  4sqlem13m  12966  4sqlem16  12969  4sqlem17  12970  4sqlem18  12971  ctiunctlemfo  13050  ptex  13337  prdsval  13346  prdsbas  13349  prdsbascl  13362  mgmsscl  13434  subsubm  13556  mhmima  13564  imasgrp2  13687  mhmmnd  13693  mulgdir  13731  subgmulg  13765  issubg2m  13766  issubgrpd2  13767  grpissubg  13771  subsubg  13774  isnsg3  13784  ssnmz  13788  eqger  13801  eqgen  13804  ecqusaddcl  13816  ghmrn  13834  ghmnsgima  13845  conjsubg  13854  conjnmz  13856  ring1  14062  dvdsrvald  14097  dvdsrd  14098  dvdsrex  14102  0unit  14133  invrpropdg  14153  lringuplu  14200  subrngin  14217  subsubrng  14218  subrgcrng  14229  subrgin  14248  subsubrg  14249  islmodd  14297  lssvacl  14369  lssvancl1  14371  lss0cl  14373  lssvscl  14379  lssvnegcl  14380  lssincl  14389  issubrgd  14456  lidlrsppropdg  14499  2idlcpblrng  14527  zsssubrg  14589  unopn  14719  tsettps  14752  tgss2  14793  difopn  14822  resttop  14884  resttopon  14885  restco  14888  tgcn  14922  tgcnp  14923  cnptopco  14936  upxp  14986  txcn  14989  txdis  14991  cnmpt11  14997  cnmpt11f  14998  cnmpt1t  14999  cnmpt12  15001  cnmpt21  15005  cnmpt21f  15006  cnmpt2t  15007  cnmpt22  15008  cnmpt22f  15009  cnmpt1res  15010  xmeter  15150  mscl  15179  xmscl  15180  bdxmet  15215  cncfmpt1f  15312  cdivcncfap  15318  negfcncf  15320  ivthreinc  15359  cnmptlimc  15388  dvcnp2cntop  15413  elplyd  15455  plypow  15458  plyconst  15459  plyaddlem1  15461  plysub  15467  dvply2g  15480  sincn  15483  coscn  15484  relogcl  15576  mpodvdsmulf1o  15704  fsumdvdsmul  15705  mersenne  15711  perfect  15715  lgsne0  15757  lgseisenlem4  15792  lgsquadlem1  15796  usgr1vr  16087  isclwwlkn  16208  clwwlknon  16224  pwtrufal  16534