Theorem eqeltrrd 2285

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  3eltr3d  2290  exmid01  4258  pwntru  4259  xpexr2m  5143  funimaexg  5377  fvmptdv2  5692  ffvresb  5766  iotaexel  5927  2ndrn  6292  1st2ndbr  6293  elopabi  6304  cnvf1olem  6333  dftpos4  6372  tfrlemibxssdm  6436  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  nnmordi  6625  th3qlem1  6747  infiexmid  7000  onunsnss  7040  ssfirab  7059  ssfidc  7060  fnfi  7064  fidcenumlemr  7083  elfi2  7100  ordiso2  7163  djulclb  7183  ctmlemr  7236  ctssdccl  7239  ctssdc  7241  exmidfodomrlemreseldju  7339  exmidfodomrlemr  7341  pw1m  7370  exmidapne  7407  archnqq  7565  prarloclemarch2  7567  enq0tr  7582  nqnq0  7589  addcmpblnq0  7591  mulcmpblnq0  7592  mulcanenq0ec  7593  addclnq0  7599  mulclnq0  7600  nqpnq0nq  7601  nq0m0r  7604  distrnq0  7607  addassnq0lemcl  7609  prarloclemlt  7641  prarloclem5  7648  distrlem4prl  7732  distrlem4pru  7733  ltexprlemm  7748  ltexprlemrl  7758  ltexprlemru  7760  addcanprleml  7762  cauappcvgprlemladdru  7804  prsrlem1  7890  mulgt0sr  7926  axpre-suploclemres  8049  cnegexlem2  8283  subf  8309  resubcl  8371  negcon1ad  8413  subeq0bd  8486  rimul  8693  rereim  8694  aprcl  8754  nn0nnaddcl  9361  elnn0nn  9372  zaddcllemneg  9446  zsubcl  9448  zrevaddcl  9458  elz2  9479  zdiv  9496  peano5uzti  9516  peano2uzr  9741  uzaddcl  9742  divfnzn  9777  qsubcl  9794  qrevaddcl  9800  fseq1p1m1  10251  suprzubdc  10416  modqmuladdim  10549  frec2uzrand  10587  frecuzrdglem  10593  frecuzrdg0  10595  frecuzrdgdomlem  10599  frecuzrdg0t  10604  frecuzrdgsuctlem  10605  seq3val  10642  seq3feq  10662  iseqf1olemnab  10683  seqf1oglem2  10702  seqfeq3  10711  seqfeq4g  10713  expaddzaplem  10764  expaddzap  10765  expmulzap  10767  zesq  10840  bcm1k  10942  bccl  10949  permnn  10953  seq3coll  11024  ccatrn  11103  shftuz  11243  ref  11281  imf  11282  crre  11283  rereb  11289  resqrexlemnm  11444  absf  11536  summodclem2a  11807  summodc  11809  fsumgcl  11812  fsum3  11813  fsumf1o  11816  fsumcnv  11863  mptfzshft  11868  isumlessdc  11922  geolim2  11938  prodmodclem3  12001  fprodseq  12009  fprodf1o  12014  dvdsaddre2b  12267  3dvds  12290  oexpneg  12303  nn0ob  12334  divalglemqt  12345  gcdf  12408  lcmgcdlem  12514  sqnprm  12573  sqrt2irrlem  12598  2sqpwodd  12613  fnum  12627  fden  12628  phimullem  12662  pc2dvds  12768  gzsubcl  12818  4sqlem5  12820  4sqlem9  12824  4sqlem10  12825  mul4sqlem  12831  mul4sq  12832  4sqlem11  12839  4sqlem13m  12841  4sqlem16  12844  4sqlem17  12845  4sqlem18  12846  ctiunctlemfo  12925  ptex  13211  prdsval  13220  prdsbas  13223  prdsbascl  13236  mgmsscl  13308  subsubm  13430  mhmima  13438  imasgrp2  13561  mhmmnd  13567  mulgdir  13605  subgmulg  13639  issubg2m  13640  issubgrpd2  13641  grpissubg  13645  subsubg  13648  isnsg3  13658  ssnmz  13662  eqger  13675  eqgen  13678  ecqusaddcl  13690  ghmrn  13708  ghmnsgima  13719  conjsubg  13728  conjnmz  13730  ring1  13936  reldvdsrsrg  13969  dvdsrvald  13970  dvdsrd  13971  dvdsrex  13975  0unit  14006  invrpropdg  14026  lringuplu  14073  subrngin  14090  subsubrng  14091  subrgcrng  14102  subrgin  14121  subsubrg  14122  islmodd  14170  lssvacl  14242  lssvancl1  14244  lss0cl  14246  lssvscl  14252  lssvnegcl  14253  lssincl  14262  issubrgd  14329  lidlrsppropdg  14372  2idlcpblrng  14400  zsssubrg  14462  unopn  14592  tsettps  14625  tgss2  14666  difopn  14695  resttop  14757  resttopon  14758  restco  14761  tgcn  14795  tgcnp  14796  cnptopco  14809  upxp  14859  txcn  14862  txdis  14864  cnmpt11  14870  cnmpt11f  14871  cnmpt1t  14872  cnmpt12  14874  cnmpt21  14878  cnmpt21f  14879  cnmpt2t  14880  cnmpt22  14881  cnmpt22f  14882  cnmpt1res  14883  xmeter  15023  mscl  15052  xmscl  15053  bdxmet  15088  cncfmpt1f  15185  cdivcncfap  15191  negfcncf  15193  ivthreinc  15232  cnmptlimc  15261  dvcnp2cntop  15286  elplyd  15328  plypow  15331  plyconst  15332  plyaddlem1  15334  plysub  15340  dvply2g  15353  sincn  15356  coscn  15357  relogcl  15449  mpodvdsmulf1o  15577  fsumdvdsmul  15578  mersenne  15584  perfect  15588  lgsne0  15630  lgseisenlem4  15665  lgsquadlem1  15669  pwtrufal  16136