Theorem eqeltrrd 2271

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

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

This theorem is referenced by:  3eltr3d  2276  exmid01  4228  pwntru  4229  xpexr2m  5108  funimaexg  5339  fvmptdv2  5648  ffvresb  5722  iotaexel  5879  2ndrn  6238  1st2ndbr  6239  elopabi  6250  cnvf1olem  6279  dftpos4  6318  tfrlemibxssdm  6382  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  nnmordi  6571  th3qlem1  6693  infiexmid  6935  onunsnss  6975  ssfirab  6992  ssfidc  6993  fnfi  6997  fidcenumlemr  7016  elfi2  7033  ordiso2  7096  djulclb  7116  ctmlemr  7169  ctssdccl  7172  ctssdc  7174  exmidfodomrlemreseldju  7262  exmidfodomrlemr  7264  exmidapne  7322  archnqq  7479  prarloclemarch2  7481  enq0tr  7496  nqnq0  7503  addcmpblnq0  7505  mulcmpblnq0  7506  mulcanenq0ec  7507  addclnq0  7513  mulclnq0  7514  nqpnq0nq  7515  nq0m0r  7518  distrnq0  7521  addassnq0lemcl  7523  prarloclemlt  7555  prarloclem5  7562  distrlem4prl  7646  distrlem4pru  7647  ltexprlemm  7662  ltexprlemrl  7672  ltexprlemru  7674  addcanprleml  7676  cauappcvgprlemladdru  7718  prsrlem1  7804  mulgt0sr  7840  axpre-suploclemres  7963  cnegexlem2  8197  subf  8223  resubcl  8285  negcon1ad  8327  subeq0bd  8400  rimul  8606  rereim  8607  aprcl  8667  nn0nnaddcl  9274  elnn0nn  9285  zaddcllemneg  9359  zsubcl  9361  zrevaddcl  9370  elz2  9391  zdiv  9408  peano5uzti  9428  peano2uzr  9653  uzaddcl  9654  divfnzn  9689  qsubcl  9706  qrevaddcl  9712  fseq1p1m1  10163  modqmuladdim  10441  frec2uzrand  10479  frecuzrdglem  10485  frecuzrdg0  10487  frecuzrdgdomlem  10491  frecuzrdg0t  10496  frecuzrdgsuctlem  10497  seq3val  10534  seq3feq  10554  iseqf1olemnab  10575  seqf1oglem2  10594  seqfeq3  10603  seqfeq4g  10605  expaddzaplem  10656  expaddzap  10657  expmulzap  10659  zesq  10732  bcm1k  10834  bccl  10841  permnn  10845  seq3coll  10916  shftuz  10964  ref  11002  imf  11003  crre  11004  rereb  11010  resqrexlemnm  11165  absf  11257  summodclem2a  11527  summodc  11529  fsumgcl  11532  fsum3  11533  fsumf1o  11536  fsumcnv  11583  mptfzshft  11588  isumlessdc  11642  geolim2  11658  prodmodclem3  11721  fprodseq  11729  fprodf1o  11734  dvdsaddre2b  11987  oexpneg  12021  nn0ob  12052  divalglemqt  12063  suprzubdc  12092  gcdf  12112  lcmgcdlem  12218  sqnprm  12277  sqrt2irrlem  12302  2sqpwodd  12317  fnum  12331  fden  12332  phimullem  12366  pc2dvds  12471  gzsubcl  12521  4sqlem5  12523  4sqlem9  12527  4sqlem10  12528  mul4sqlem  12534  mul4sq  12535  4sqlem11  12542  4sqlem13m  12544  4sqlem16  12547  4sqlem17  12548  4sqlem18  12549  ctiunctlemfo  12599  ptex  12878  mgmsscl  12947  subsubm  13058  mhmima  13066  imasgrp2  13183  mhmmnd  13189  mulgdir  13227  subgmulg  13261  issubg2m  13262  issubgrpd2  13263  grpissubg  13267  subsubg  13270  isnsg3  13280  ssnmz  13284  eqger  13297  eqgen  13300  ecqusaddcl  13312  ghmrn  13330  ghmnsgima  13341  conjsubg  13350  conjnmz  13352  ring1  13558  reldvdsrsrg  13591  dvdsrvald  13592  dvdsrd  13593  dvdsrex  13597  0unit  13628  invrpropdg  13648  lringuplu  13695  subrngin  13712  subsubrng  13713  subrgcrng  13724  subrgin  13743  subsubrg  13744  islmodd  13792  lssvacl  13864  lssvancl1  13866  lss0cl  13868  lssvscl  13874  lssvnegcl  13875  lssincl  13884  issubrgd  13951  lidlrsppropdg  13994  2idlcpblrng  14022  zsssubrg  14084  unopn  14184  tsettps  14217  tgss2  14258  difopn  14287  resttop  14349  resttopon  14350  restco  14353  tgcn  14387  tgcnp  14388  cnptopco  14401  upxp  14451  txcn  14454  txdis  14456  cnmpt11  14462  cnmpt11f  14463  cnmpt1t  14464  cnmpt12  14466  cnmpt21  14470  cnmpt21f  14471  cnmpt2t  14472  cnmpt22  14473  cnmpt22f  14474  cnmpt1res  14475  xmeter  14615  mscl  14644  xmscl  14645  bdxmet  14680  cncfmpt1f  14777  cdivcncfap  14783  negfcncf  14785  ivthreinc  14824  cnmptlimc  14853  dvcnp2cntop  14878  elplyd  14920  plypow  14923  plyconst  14924  plyaddlem1  14926  plysub  14932  sincn  14945  coscn  14946  relogcl  15038  lgsne0  15195  lgseisenlem4  15230  lgsquadlem1  15234  pwtrufal  15558