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  8502  subf  8528  resubcl  8590  negcon1ad  8632  subeq0bd  8706  rimul  8913  rereim  8914  aprcl  8974  nn0nnaddcl  9594  elnn0nn  9605  zaddcllemneg  9683  zsubcl  9685  zrevaddcl  9695  elz2  9716  zdiv  9734  peano5uzti  9754  peano2uzr  9985  uzaddcl  9986  divfnzn  10021  qsubcl  10038  qrevaddcl  10044  fseq1p1m1  10501  suprzubdc  10671  modqmuladdim  10804  frec2uzrand  10842  frecuzrdglem  10848  frecuzrdg0  10850  frecuzrdgdomlem  10854  frecuzrdg0t  10859  frecuzrdgsuctlem  10860  seq3val  10897  seq3feq  10917  iseqf1olemnab  10938  seqf1oglem2  10957  seqfeq3  10966  seqfeq4g  10968  expaddzaplem  11019  expaddzap  11020  expmulzap  11022  zesq  11096  bcm1k  11198  bccl  11205  permnn  11210  hashf1lem2  11286  hashf1  11287  seq3coll  11294  ccatrn  11377  shftuz  11582  ref  11620  imf  11621  crre  11622  rereb  11628  resqrexlemnm  11784  absf  11876  summodclem2a  12148  summodc  12150  fsumgcl  12153  fsum3  12154  fsumf1o  12157  fsumcnv  12204  mptfzshft  12209  isumlessdc  12263  geolim2  12279  prodmodclem3  12342  fprodseq  12350  fprodf1o  12355  dvdsaddre2b  12608  3dvds  12631  oexpneg  12644  nn0ob  12675  divalglemqt  12686  gcdf  12749  lcmgcdlem  12855  sqnprm  12914  sqrt2irrlem  12939  2sqpwodd  12954  fnum  12968  fden  12969  phimullem  13003  pc2dvds  13109  gzsubcl  13159  4sqlem5  13161  4sqlem9  13165  4sqlem10  13166  mul4sqlem  13172  mul4sq  13173  4sqlem11  13180  4sqlem13m  13182  4sqlem16  13185  4sqlem17  13186  4sqlem18  13187  ballotfilem2  13228  ballotfilemsf1o  13257  ballotfilemrinv0  13276  ctiunctlemfo  13330  ptex  13618  mgmsscl  13681  subsubm  13790  mhmima  13798  imasgrp2  13913  mhmmnd  13919  mulgdir  13957  subgmulg  13991  issubg2m  13992  issubgrpd2  13993  grpissubg  13997  subsubg  14000  isnsg3  14010  ssnmz  14014  eqger  14027  eqgen  14030  ecqusaddcl  14042  ghmrn  14060  ghmnsgima  14071  conjsubg  14080  conjnmz  14082  gsumclfi  14159  gsumsubmclfi  14163  prdsval  14173  prdsbas  14176  prdsbascl  14189  ring1  14364  dvdsrvald  14400  dvdsrd  14401  dvdsrex  14405  0unit  14436  invrpropdg  14456  lringuplu  14503  subrngin  14521  subsubrng  14522  subrgcrng  14533  subrgin  14552  subsubrg  14553  aprnzr  14599  aprlring  14600  islmodd  14629  lssvacl  14702  lssvancl1  14704  lss0cl  14706  lssvscl  14712  lssvnegcl  14713  lssincl  14722  issubrgd  14789  lidlrsppropdg  14832  2idlcpblrng  14860  zsssubrg  14922  issubassa2  15035  unopn  15106  tsettps  15139  tgss2  15180  difopn  15209  resttop  15271  resttopon  15272  restco  15275  tgcn  15309  tgcnp  15310  cnptopco  15323  upxp  15373  txcn  15376  txdis  15378  cnmpt11  15384  cnmpt11f  15385  cnmpt1t  15386  cnmpt12  15388  cnmpt21  15392  cnmpt21f  15393  cnmpt2t  15394  cnmpt22  15395  cnmpt22f  15396  cnmpt1res  15397  xmeter  15537  mscl  15566  xmscl  15567  bdxmet  15602  cncfmpt1f  15699  cdivcncfap  15705  negfcncf  15707  ivthreinc  15746  cnmptlimc  15775  dvcnp2cntop  15800  elplyd  15842  plypow  15845  plyconst  15846  plyaddlem1  15848  plysub  15854  dvply2g  15867  sincn  15870  coscn  15871  relogcl  15963  mpodvdsmulf1o  16104  fsumdvdsmul  16105  mersenne  16111  perfect  16115  lgsne0  16157  lgseisenlem4  16192  lgsquadlem1  16196  usgr1vr  16489  p1evtxdeqfilem  16552  isclwwlkn  16654  clwwlknon  16670  pwtrufal  17027  repiecele0  17075  qdiff  17098