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  5652  ffvresb  5726  iotaexel  5883  2ndrn  6242  1st2ndbr  6243  elopabi  6254  cnvf1olem  6283  dftpos4  6322  tfrlemibxssdm  6386  tfr1onlembxssdm  6402  tfrcllembxssdm  6415  nnmordi  6575  th3qlem1  6697  infiexmid  6939  onunsnss  6979  ssfirab  6998  ssfidc  6999  fnfi  7003  fidcenumlemr  7022  elfi2  7039  ordiso2  7102  djulclb  7122  ctmlemr  7175  ctssdccl  7178  ctssdc  7180  exmidfodomrlemreseldju  7269  exmidfodomrlemr  7271  exmidapne  7329  archnqq  7486  prarloclemarch2  7488  enq0tr  7503  nqnq0  7510  addcmpblnq0  7512  mulcmpblnq0  7513  mulcanenq0ec  7514  addclnq0  7520  mulclnq0  7521  nqpnq0nq  7522  nq0m0r  7525  distrnq0  7528  addassnq0lemcl  7530  prarloclemlt  7562  prarloclem5  7569  distrlem4prl  7653  distrlem4pru  7654  ltexprlemm  7669  ltexprlemrl  7679  ltexprlemru  7681  addcanprleml  7683  cauappcvgprlemladdru  7725  prsrlem1  7811  mulgt0sr  7847  axpre-suploclemres  7970  cnegexlem2  8204  subf  8230  resubcl  8292  negcon1ad  8334  subeq0bd  8407  rimul  8614  rereim  8615  aprcl  8675  nn0nnaddcl  9282  elnn0nn  9293  zaddcllemneg  9367  zsubcl  9369  zrevaddcl  9378  elz2  9399  zdiv  9416  peano5uzti  9436  peano2uzr  9661  uzaddcl  9662  divfnzn  9697  qsubcl  9714  qrevaddcl  9720  fseq1p1m1  10171  suprzubdc  10328  modqmuladdim  10461  frec2uzrand  10499  frecuzrdglem  10505  frecuzrdg0  10507  frecuzrdgdomlem  10511  frecuzrdg0t  10516  frecuzrdgsuctlem  10517  seq3val  10554  seq3feq  10574  iseqf1olemnab  10595  seqf1oglem2  10614  seqfeq3  10623  seqfeq4g  10625  expaddzaplem  10676  expaddzap  10677  expmulzap  10679  zesq  10752  bcm1k  10854  bccl  10861  permnn  10865  seq3coll  10936  shftuz  10984  ref  11022  imf  11023  crre  11024  rereb  11030  resqrexlemnm  11185  absf  11277  summodclem2a  11548  summodc  11550  fsumgcl  11553  fsum3  11554  fsumf1o  11557  fsumcnv  11604  mptfzshft  11609  isumlessdc  11663  geolim2  11679  prodmodclem3  11742  fprodseq  11750  fprodf1o  11755  dvdsaddre2b  12008  3dvds  12031  oexpneg  12044  nn0ob  12075  divalglemqt  12086  gcdf  12149  lcmgcdlem  12255  sqnprm  12314  sqrt2irrlem  12339  2sqpwodd  12354  fnum  12368  fden  12369  phimullem  12403  pc2dvds  12509  gzsubcl  12559  4sqlem5  12561  4sqlem9  12565  4sqlem10  12566  mul4sqlem  12572  mul4sq  12573  4sqlem11  12580  4sqlem13m  12582  4sqlem16  12585  4sqlem17  12586  4sqlem18  12587  ctiunctlemfo  12666  ptex  12945  mgmsscl  13014  subsubm  13125  mhmima  13133  imasgrp2  13250  mhmmnd  13256  mulgdir  13294  subgmulg  13328  issubg2m  13329  issubgrpd2  13330  grpissubg  13334  subsubg  13337  isnsg3  13347  ssnmz  13351  eqger  13364  eqgen  13367  ecqusaddcl  13379  ghmrn  13397  ghmnsgima  13408  conjsubg  13417  conjnmz  13419  ring1  13625  reldvdsrsrg  13658  dvdsrvald  13659  dvdsrd  13660  dvdsrex  13664  0unit  13695  invrpropdg  13715  lringuplu  13762  subrngin  13779  subsubrng  13780  subrgcrng  13791  subrgin  13810  subsubrg  13811  islmodd  13859  lssvacl  13931  lssvancl1  13933  lss0cl  13935  lssvscl  13941  lssvnegcl  13942  lssincl  13951  issubrgd  14018  lidlrsppropdg  14061  2idlcpblrng  14089  zsssubrg  14151  unopn  14251  tsettps  14284  tgss2  14325  difopn  14354  resttop  14416  resttopon  14417  restco  14420  tgcn  14454  tgcnp  14455  cnptopco  14468  upxp  14518  txcn  14521  txdis  14523  cnmpt11  14529  cnmpt11f  14530  cnmpt1t  14531  cnmpt12  14533  cnmpt21  14537  cnmpt21f  14538  cnmpt2t  14539  cnmpt22  14540  cnmpt22f  14541  cnmpt1res  14542  xmeter  14682  mscl  14711  xmscl  14712  bdxmet  14747  cncfmpt1f  14844  cdivcncfap  14850  negfcncf  14852  ivthreinc  14891  cnmptlimc  14920  dvcnp2cntop  14945  elplyd  14987  plypow  14990  plyconst  14991  plyaddlem1  14993  plysub  14999  dvply2g  15012  sincn  15015  coscn  15016  relogcl  15108  mpodvdsmulf1o  15236  fsumdvdsmul  15237  mersenne  15243  perfect  15247  lgsne0  15289  lgseisenlem4  15324  lgsquadlem1  15328  pwtrufal  15652