Theorem eqeltrrd 2274

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  3eltr3d  2279  exmid01  4232  pwntru  4233  xpexr2m  5112  funimaexg  5343  fvmptdv2  5654  ffvresb  5728  iotaexel  5885  2ndrn  6250  1st2ndbr  6251  elopabi  6262  cnvf1olem  6291  dftpos4  6330  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  nnmordi  6583  th3qlem1  6705  infiexmid  6947  onunsnss  6987  ssfirab  7006  ssfidc  7007  fnfi  7011  fidcenumlemr  7030  elfi2  7047  ordiso2  7110  djulclb  7130  ctmlemr  7183  ctssdccl  7186  ctssdc  7188  exmidfodomrlemreseldju  7281  exmidfodomrlemr  7283  exmidapne  7345  archnqq  7503  prarloclemarch2  7505  enq0tr  7520  nqnq0  7527  addcmpblnq0  7529  mulcmpblnq0  7530  mulcanenq0ec  7531  addclnq0  7537  mulclnq0  7538  nqpnq0nq  7539  nq0m0r  7542  distrnq0  7545  addassnq0lemcl  7547  prarloclemlt  7579  prarloclem5  7586  distrlem4prl  7670  distrlem4pru  7671  ltexprlemm  7686  ltexprlemrl  7696  ltexprlemru  7698  addcanprleml  7700  cauappcvgprlemladdru  7742  prsrlem1  7828  mulgt0sr  7864  axpre-suploclemres  7987  cnegexlem2  8221  subf  8247  resubcl  8309  negcon1ad  8351  subeq0bd  8424  rimul  8631  rereim  8632  aprcl  8692  nn0nnaddcl  9299  elnn0nn  9310  zaddcllemneg  9384  zsubcl  9386  zrevaddcl  9395  elz2  9416  zdiv  9433  peano5uzti  9453  peano2uzr  9678  uzaddcl  9679  divfnzn  9714  qsubcl  9731  qrevaddcl  9737  fseq1p1m1  10188  suprzubdc  10345  modqmuladdim  10478  frec2uzrand  10516  frecuzrdglem  10522  frecuzrdg0  10524  frecuzrdgdomlem  10528  frecuzrdg0t  10533  frecuzrdgsuctlem  10534  seq3val  10571  seq3feq  10591  iseqf1olemnab  10612  seqf1oglem2  10631  seqfeq3  10640  seqfeq4g  10642  expaddzaplem  10693  expaddzap  10694  expmulzap  10696  zesq  10769  bcm1k  10871  bccl  10878  permnn  10882  seq3coll  10953  shftuz  11001  ref  11039  imf  11040  crre  11041  rereb  11047  resqrexlemnm  11202  absf  11294  summodclem2a  11565  summodc  11567  fsumgcl  11570  fsum3  11571  fsumf1o  11574  fsumcnv  11621  mptfzshft  11626  isumlessdc  11680  geolim2  11696  prodmodclem3  11759  fprodseq  11767  fprodf1o  11772  dvdsaddre2b  12025  3dvds  12048  oexpneg  12061  nn0ob  12092  divalglemqt  12103  gcdf  12166  lcmgcdlem  12272  sqnprm  12331  sqrt2irrlem  12356  2sqpwodd  12371  fnum  12385  fden  12386  phimullem  12420  pc2dvds  12526  gzsubcl  12576  4sqlem5  12578  4sqlem9  12582  4sqlem10  12583  mul4sqlem  12589  mul4sq  12590  4sqlem11  12597  4sqlem13m  12599  4sqlem16  12602  4sqlem17  12603  4sqlem18  12604  ctiunctlemfo  12683  ptex  12968  prdsval  12977  prdsbas  12980  prdsbascl  12993  mgmsscl  13065  subsubm  13187  mhmima  13195  imasgrp2  13318  mhmmnd  13324  mulgdir  13362  subgmulg  13396  issubg2m  13397  issubgrpd2  13398  grpissubg  13402  subsubg  13405  isnsg3  13415  ssnmz  13419  eqger  13432  eqgen  13435  ecqusaddcl  13447  ghmrn  13465  ghmnsgima  13476  conjsubg  13485  conjnmz  13487  ring1  13693  reldvdsrsrg  13726  dvdsrvald  13727  dvdsrd  13728  dvdsrex  13732  0unit  13763  invrpropdg  13783  lringuplu  13830  subrngin  13847  subsubrng  13848  subrgcrng  13859  subrgin  13878  subsubrg  13879  islmodd  13927  lssvacl  13999  lssvancl1  14001  lss0cl  14003  lssvscl  14009  lssvnegcl  14010  lssincl  14019  issubrgd  14086  lidlrsppropdg  14129  2idlcpblrng  14157  zsssubrg  14219  unopn  14349  tsettps  14382  tgss2  14423  difopn  14452  resttop  14514  resttopon  14515  restco  14518  tgcn  14552  tgcnp  14553  cnptopco  14566  upxp  14616  txcn  14619  txdis  14621  cnmpt11  14627  cnmpt11f  14628  cnmpt1t  14629  cnmpt12  14631  cnmpt21  14635  cnmpt21f  14636  cnmpt2t  14637  cnmpt22  14638  cnmpt22f  14639  cnmpt1res  14640  xmeter  14780  mscl  14809  xmscl  14810  bdxmet  14845  cncfmpt1f  14942  cdivcncfap  14948  negfcncf  14950  ivthreinc  14989  cnmptlimc  15018  dvcnp2cntop  15043  elplyd  15085  plypow  15088  plyconst  15089  plyaddlem1  15091  plysub  15097  dvply2g  15110  sincn  15113  coscn  15114  relogcl  15206  mpodvdsmulf1o  15334  fsumdvdsmul  15335  mersenne  15341  perfect  15345  lgsne0  15387  lgseisenlem4  15422  lgsquadlem1  15426  pwtrufal  15752