Theorem eqeltrrd 2316

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  3eltr3d  2321  exmid01  4335  pwntru  4336  xpexr2m  5229  funimaexg  5465  fndmexd  5581  fvmptdv2  5795  ffvresb  5871  iotaexel  6043  2ndrn  6417  1st2ndbr  6418  elopabi  6431  cnvf1olem  6460  dftpos4  6534  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  nnmordi  6789  th3qlem1  6911  infiexmid  7181  onunsnss  7224  ssfirab  7244  ssfidc  7245  fnfi  7250  fidcenumlemr  7272  elfi2  7306  f1setfi  7317  ordiso2  7375  djulclb  7395  ctmlemr  7448  ctssdccl  7451  ctssdc  7453  exmidfodomrlemreseldju  7552  exmidfodomrlemr  7554  pw1m  7583  exmidapne  7626  archnqq  7784  prarloclemarch2  7786  enq0tr  7801  nqnq0  7808  addcmpblnq0  7810  mulcmpblnq0  7811  mulcanenq0ec  7812  addclnq0  7818  mulclnq0  7819  nqpnq0nq  7820  nq0m0r  7823  distrnq0  7826  addassnq0lemcl  7828  prarloclemlt  7860  prarloclem5  7867  distrlem4prl  7951  distrlem4pru  7952  ltexprlemm  7967  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  cauappcvgprlemladdru  8023  prsrlem1  8109  mulgt0sr  8145  axpre-suploclemres  8268  cnegexlem2  8503  subf  8529  resubcl  8591  negcon1ad  8633  subeq0bd  8707  rimul  8915  rereim  8916  aprcl  8976  nn0nnaddcl  9598  elnn0nn  9609  zaddcllemneg  9687  zsubcl  9689  zrevaddcl  9699  elz2  9720  zdiv  9738  peano5uzti  9758  peano2uzr  9994  uzaddcl  9995  divfnzn  10030  qsubcl  10047  qrevaddcl  10053  fseq1p1m1  10511  suprzubdc  10681  modqmuladdim  10817  frec2uzrand  10855  frecuzrdglem  10861  frecuzrdg0  10863  frecuzrdgdomlem  10867  frecuzrdg0t  10872  frecuzrdgsuctlem  10873  seq3val  10910  seq3feq  10930  iseqf1olemnab  10951  seqf1oglem2  10970  seqfeq3  10979  seqfeq4g  10981  expaddzaplem  11032  expaddzap  11033  expmulzap  11035  zesq  11109  bcm1k  11212  bccl  11219  permnn  11224  hashf1lem2  11300  hashf1  11301  seq3coll  11308  ccatrn  11391  shftuz  11596  ref  11634  imf  11635  crre  11636  rereb  11642  resqrexlemnm  11798  absf  11891  summodclem2a  12164  summodc  12166  fsumgcl  12169  fsum3  12170  fsumf1o  12173  fsumcnv  12220  mptfzshft  12225  isumlessdc  12279  geolim2  12295  prodmodclem3  12358  fprodseq  12366  fprodf1o  12371  dvdsaddre2b  12624  3dvds  12647  oexpneg  12660  nn0ob  12691  divalglemqt  12702  gcdf  12765  lcmgcdlem  12871  sqnprm  12931  sqrt2irrlem  12956  2sqpwodd  12972  fnum  12986  fden  12987  nn0sqdcq  13004  phimullem  13023  pc2dvds  13129  gzsubcl  13179  4sqlem5  13181  4sqlem9  13185  4sqlem10  13186  mul4sqlem  13192  mul4sq  13193  4sqlem11  13200  4sqlem13m  13202  4sqlem16  13205  4sqlem17  13206  4sqlem18  13207  ballotfilem2  13277  ballotfilemsf1o  13306  ballotfilemrinv0  13325  ctiunctlemfo  13379  ptex  13667  mgmsscl  13730  subsubm  13839  mhmima  13847  imasgrp2  13962  mhmmnd  13968  mulgdir  14006  subgmulg  14040  issubg2m  14041  issubgrpd2  14042  grpissubg  14046  subsubg  14049  isnsg3  14059  ssnmz  14063  eqger  14076  eqgen  14079  ecqusaddcl  14091  ghmrn  14109  ghmnsgima  14120  conjsubg  14129  conjnmz  14131  gsumclfi  14208  gsumsubmclfi  14212  prdsval  14222  prdsbas  14225  prdsbascl  14238  ring1  14413  dvdsrvald  14449  dvdsrd  14450  dvdsrex  14454  0unit  14485  invrpropdg  14505  lringuplu  14552  subrngin  14570  subsubrng  14571  subrgcrng  14582  subrgin  14601  subsubrg  14602  aprnzr  14648  aprlring  14649  islmodd  14678  lssvacl  14751  lssvancl1  14753  lss0cl  14755  lssvscl  14761  lssvnegcl  14762  lssincl  14771  issubrgd  14838  lidlrsppropdg  14881  2idlcpblrng  14909  zsssubrg  14971  issubassa2  15084  unopn  15155  tsettps  15188  tgss2  15229  difopn  15258  resttop  15320  resttopon  15321  restco  15324  tgcn  15358  tgcnp  15359  cnptopco  15372  upxp  15422  txcn  15425  txdis  15427  cnmpt11  15433  cnmpt11f  15434  cnmpt1t  15435  cnmpt12  15437  cnmpt21  15441  cnmpt21f  15442  cnmpt2t  15443  cnmpt22  15444  cnmpt22f  15445  cnmpt1res  15446  xmeter  15586  mscl  15615  xmscl  15616  bdxmet  15651  cncfmpt1f  15748  cdivcncfap  15754  negfcncf  15756  ivthreinc  15795  cnmptlimc  15824  dvcnp2cntop  15849  elplyd  15891  plypow  15894  plyconst  15895  plyaddlem1  15897  plysub  15903  dvply2g  15916  sincn  15919  coscn  15920  relogcl  16013  ppiprm  16170  ppinprm  16171  mpodvdsmulf1o  16185  fsumdvdsmul  16186  mersenne  16195  perfect  16199  lgsne0  16255  lgseisenlem4  16290  lgsquadlem1  16294  usgr1vr  16587  p1evtxdeqfilem  16650  isclwwlkn  16752  clwwlknon  16768  pwtrufal  17125  repiecele0  17173  qdiff  17196