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  4282  pwntru  4283  xpexr2m  5170  funimaexg  5405  fvmptdv2  5726  ffvresb  5800  iotaexel  5965  2ndrn  6335  1st2ndbr  6336  elopabi  6347  cnvf1olem  6376  dftpos4  6415  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  nnmordi  6670  th3qlem1  6792  infiexmid  7047  onunsnss  7090  ssfirab  7109  ssfidc  7110  fnfi  7114  fidcenumlemr  7133  elfi2  7150  ordiso2  7213  djulclb  7233  ctmlemr  7286  ctssdccl  7289  ctssdc  7291  exmidfodomrlemreseldju  7389  exmidfodomrlemr  7391  pw1m  7420  exmidapne  7457  archnqq  7615  prarloclemarch2  7617  enq0tr  7632  nqnq0  7639  addcmpblnq0  7641  mulcmpblnq0  7642  mulcanenq0ec  7643  addclnq0  7649  mulclnq0  7650  nqpnq0nq  7651  nq0m0r  7654  distrnq0  7657  addassnq0lemcl  7659  prarloclemlt  7691  prarloclem5  7698  distrlem4prl  7782  distrlem4pru  7783  ltexprlemm  7798  ltexprlemrl  7808  ltexprlemru  7810  addcanprleml  7812  cauappcvgprlemladdru  7854  prsrlem1  7940  mulgt0sr  7976  axpre-suploclemres  8099  cnegexlem2  8333  subf  8359  resubcl  8421  negcon1ad  8463  subeq0bd  8536  rimul  8743  rereim  8744  aprcl  8804  nn0nnaddcl  9411  elnn0nn  9422  zaddcllemneg  9496  zsubcl  9498  zrevaddcl  9508  elz2  9529  zdiv  9546  peano5uzti  9566  peano2uzr  9792  uzaddcl  9793  divfnzn  9828  qsubcl  9845  qrevaddcl  9851  fseq1p1m1  10302  suprzubdc  10468  modqmuladdim  10601  frec2uzrand  10639  frecuzrdglem  10645  frecuzrdg0  10647  frecuzrdgdomlem  10651  frecuzrdg0t  10656  frecuzrdgsuctlem  10657  seq3val  10694  seq3feq  10714  iseqf1olemnab  10735  seqf1oglem2  10754  seqfeq3  10763  seqfeq4g  10765  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  zesq  10892  bcm1k  10994  bccl  11001  permnn  11005  seq3coll  11077  ccatrn  11157  shftuz  11344  ref  11382  imf  11383  crre  11384  rereb  11390  resqrexlemnm  11545  absf  11637  summodclem2a  11908  summodc  11910  fsumgcl  11913  fsum3  11914  fsumf1o  11917  fsumcnv  11964  mptfzshft  11969  isumlessdc  12023  geolim2  12039  prodmodclem3  12102  fprodseq  12110  fprodf1o  12115  dvdsaddre2b  12368  3dvds  12391  oexpneg  12404  nn0ob  12435  divalglemqt  12446  gcdf  12509  lcmgcdlem  12615  sqnprm  12674  sqrt2irrlem  12699  2sqpwodd  12714  fnum  12728  fden  12729  phimullem  12763  pc2dvds  12869  gzsubcl  12919  4sqlem5  12921  4sqlem9  12925  4sqlem10  12926  mul4sqlem  12932  mul4sq  12933  4sqlem11  12940  4sqlem13m  12942  4sqlem16  12945  4sqlem17  12946  4sqlem18  12947  ctiunctlemfo  13026  ptex  13313  prdsval  13322  prdsbas  13325  prdsbascl  13338  mgmsscl  13410  subsubm  13532  mhmima  13540  imasgrp2  13663  mhmmnd  13669  mulgdir  13707  subgmulg  13741  issubg2m  13742  issubgrpd2  13743  grpissubg  13747  subsubg  13750  isnsg3  13760  ssnmz  13764  eqger  13777  eqgen  13780  ecqusaddcl  13792  ghmrn  13810  ghmnsgima  13821  conjsubg  13830  conjnmz  13832  ring1  14038  dvdsrvald  14073  dvdsrd  14074  dvdsrex  14078  0unit  14109  invrpropdg  14129  lringuplu  14176  subrngin  14193  subsubrng  14194  subrgcrng  14205  subrgin  14224  subsubrg  14225  islmodd  14273  lssvacl  14345  lssvancl1  14347  lss0cl  14349  lssvscl  14355  lssvnegcl  14356  lssincl  14365  issubrgd  14432  lidlrsppropdg  14475  2idlcpblrng  14503  zsssubrg  14565  unopn  14695  tsettps  14728  tgss2  14769  difopn  14798  resttop  14860  resttopon  14861  restco  14864  tgcn  14898  tgcnp  14899  cnptopco  14912  upxp  14962  txcn  14965  txdis  14967  cnmpt11  14973  cnmpt11f  14974  cnmpt1t  14975  cnmpt12  14977  cnmpt21  14981  cnmpt21f  14982  cnmpt2t  14983  cnmpt22  14984  cnmpt22f  14985  cnmpt1res  14986  xmeter  15126  mscl  15155  xmscl  15156  bdxmet  15191  cncfmpt1f  15288  cdivcncfap  15294  negfcncf  15296  ivthreinc  15335  cnmptlimc  15364  dvcnp2cntop  15389  elplyd  15431  plypow  15434  plyconst  15435  plyaddlem1  15437  plysub  15443  dvply2g  15456  sincn  15459  coscn  15460  relogcl  15552  mpodvdsmulf1o  15680  fsumdvdsmul  15681  mersenne  15687  perfect  15691  lgsne0  15733  lgseisenlem4  15768  lgsquadlem1  15772  pwtrufal  16450