Theorem eqeltrrd 2312

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  3eltr3d  2317  exmid01  4316  pwntru  4317  xpexr2m  5209  funimaexg  5445  fndmexd  5561  fvmptdv2  5772  ffvresb  5845  iotaexel  6016  2ndrn  6390  1st2ndbr  6391  elopabi  6404  cnvf1olem  6433  dftpos4  6507  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  nnmordi  6762  th3qlem1  6884  infiexmid  7147  onunsnss  7190  ssfirab  7210  ssfidc  7211  fnfi  7216  fidcenumlemr  7238  elfi2  7272  ordiso2  7339  djulclb  7359  ctmlemr  7412  ctssdccl  7415  ctssdc  7417  exmidfodomrlemreseldju  7516  exmidfodomrlemr  7518  pw1m  7547  exmidapne  7590  archnqq  7748  prarloclemarch2  7750  enq0tr  7765  nqnq0  7772  addcmpblnq0  7774  mulcmpblnq0  7775  mulcanenq0ec  7776  addclnq0  7782  mulclnq0  7783  nqpnq0nq  7784  nq0m0r  7787  distrnq0  7790  addassnq0lemcl  7792  prarloclemlt  7824  prarloclem5  7831  distrlem4prl  7915  distrlem4pru  7916  ltexprlemm  7931  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  cauappcvgprlemladdru  7987  prsrlem1  8073  mulgt0sr  8109  axpre-suploclemres  8232  cnegexlem2  8465  subf  8491  resubcl  8553  negcon1ad  8595  subeq0bd  8669  rimul  8876  rereim  8877  aprcl  8937  nn0nnaddcl  9544  elnn0nn  9555  zaddcllemneg  9633  zsubcl  9635  zrevaddcl  9645  elz2  9666  zdiv  9684  peano5uzti  9704  peano2uzr  9935  uzaddcl  9936  divfnzn  9971  qsubcl  9988  qrevaddcl  9994  fseq1p1m1  10450  suprzubdc  10620  modqmuladdim  10753  frec2uzrand  10791  frecuzrdglem  10797  frecuzrdg0  10799  frecuzrdgdomlem  10803  frecuzrdg0t  10808  frecuzrdgsuctlem  10809  seq3val  10846  seq3feq  10866  iseqf1olemnab  10887  seqf1oglem2  10906  seqfeq3  10915  seqfeq4g  10917  expaddzaplem  10968  expaddzap  10969  expmulzap  10971  zesq  11045  bcm1k  11147  bccl  11154  permnn  11159  seq3coll  11239  ccatrn  11322  shftuz  11527  ref  11565  imf  11566  crre  11567  rereb  11573  resqrexlemnm  11728  absf  11820  summodclem2a  12092  summodc  12094  fsumgcl  12097  fsum3  12098  fsumf1o  12101  fsumcnv  12148  mptfzshft  12153  isumlessdc  12207  geolim2  12223  prodmodclem3  12286  fprodseq  12294  fprodf1o  12299  dvdsaddre2b  12552  3dvds  12575  oexpneg  12588  nn0ob  12619  divalglemqt  12630  gcdf  12693  lcmgcdlem  12799  sqnprm  12858  sqrt2irrlem  12883  2sqpwodd  12898  fnum  12912  fden  12913  phimullem  12947  pc2dvds  13053  gzsubcl  13103  4sqlem5  13105  4sqlem9  13109  4sqlem10  13110  mul4sqlem  13116  mul4sq  13117  4sqlem11  13124  4sqlem13m  13126  4sqlem16  13129  4sqlem17  13130  4sqlem18  13131  ballotfilem2  13172  ballotfilemsf1o  13201  ballotfilemrinv0  13220  ctiunctlemfo  13274  ptex  13561  mgmsscl  13624  subsubm  13738  mhmima  13746  imasgrp2  13863  mhmmnd  13869  mulgdir  13907  subgmulg  13941  issubg2m  13942  issubgrpd2  13943  grpissubg  13947  subsubg  13950  isnsg3  13960  ssnmz  13964  eqger  13977  eqgen  13980  ecqusaddcl  13992  ghmrn  14010  ghmnsgima  14021  conjsubg  14030  conjnmz  14032  gfsumcl  14110  prdsval  14115  prdsbas  14118  prdsbascl  14131  ring1  14302  dvdsrvald  14338  dvdsrd  14339  dvdsrex  14343  0unit  14374  invrpropdg  14394  lringuplu  14441  subrngin  14459  subsubrng  14460  subrgcrng  14471  subrgin  14490  subsubrg  14491  aprnzr  14537  aprlring  14538  islmodd  14567  lssvacl  14639  lssvancl1  14641  lss0cl  14643  lssvscl  14649  lssvnegcl  14650  lssincl  14659  issubrgd  14726  lidlrsppropdg  14769  2idlcpblrng  14797  zsssubrg  14859  unopn  14996  tsettps  15029  tgss2  15070  difopn  15099  resttop  15161  resttopon  15162  restco  15165  tgcn  15199  tgcnp  15200  cnptopco  15213  upxp  15263  txcn  15266  txdis  15268  cnmpt11  15274  cnmpt11f  15275  cnmpt1t  15276  cnmpt12  15278  cnmpt21  15282  cnmpt21f  15283  cnmpt2t  15284  cnmpt22  15285  cnmpt22f  15286  cnmpt1res  15287  xmeter  15427  mscl  15456  xmscl  15457  bdxmet  15492  cncfmpt1f  15589  cdivcncfap  15595  negfcncf  15597  ivthreinc  15636  cnmptlimc  15665  dvcnp2cntop  15690  elplyd  15732  plypow  15735  plyconst  15736  plyaddlem1  15738  plysub  15744  dvply2g  15757  sincn  15760  coscn  15761  relogcl  15853  mpodvdsmulf1o  15984  fsumdvdsmul  15985  mersenne  15991  perfect  15995  lgsne0  16037  lgseisenlem4  16072  lgsquadlem1  16076  usgr1vr  16369  p1evtxdeqfilem  16432  isclwwlkn  16534  clwwlknon  16550  pwtrufal  16897  repiecele0  16936  qdiff  16959