Theorem eqeltrrd 2309

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

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

This theorem is referenced by:  3eltr3d  2314  exmid01  4288  pwntru  4289  xpexr2m  5178  funimaexg  5414  fvmptdv2  5736  ffvresb  5810  iotaexel  5975  2ndrn  6345  1st2ndbr  6346  elopabi  6359  cnvf1olem  6388  dftpos4  6428  tfrlemibxssdm  6492  tfr1onlembxssdm  6508  tfrcllembxssdm  6521  nnmordi  6683  th3qlem1  6805  infiexmid  7065  onunsnss  7108  ssfirab  7128  ssfidc  7129  fnfi  7134  fidcenumlemr  7153  elfi2  7170  ordiso2  7233  djulclb  7253  ctmlemr  7306  ctssdccl  7309  ctssdc  7311  exmidfodomrlemreseldju  7410  exmidfodomrlemr  7412  pw1m  7441  exmidapne  7478  archnqq  7636  prarloclemarch2  7638  enq0tr  7653  nqnq0  7660  addcmpblnq0  7662  mulcmpblnq0  7663  mulcanenq0ec  7664  addclnq0  7670  mulclnq0  7671  nqpnq0nq  7672  nq0m0r  7675  distrnq0  7678  addassnq0lemcl  7680  prarloclemlt  7712  prarloclem5  7719  distrlem4prl  7803  distrlem4pru  7804  ltexprlemm  7819  ltexprlemrl  7829  ltexprlemru  7831  addcanprleml  7833  cauappcvgprlemladdru  7875  prsrlem1  7961  mulgt0sr  7997  axpre-suploclemres  8120  cnegexlem2  8354  subf  8380  resubcl  8442  negcon1ad  8484  subeq0bd  8557  rimul  8764  rereim  8765  aprcl  8825  nn0nnaddcl  9432  elnn0nn  9443  zaddcllemneg  9517  zsubcl  9519  zrevaddcl  9529  elz2  9550  zdiv  9567  peano5uzti  9587  peano2uzr  9818  uzaddcl  9819  divfnzn  9854  qsubcl  9871  qrevaddcl  9877  fseq1p1m1  10328  suprzubdc  10495  modqmuladdim  10628  frec2uzrand  10666  frecuzrdglem  10672  frecuzrdg0  10674  frecuzrdgdomlem  10678  frecuzrdg0t  10683  frecuzrdgsuctlem  10684  seq3val  10721  seq3feq  10741  iseqf1olemnab  10762  seqf1oglem2  10781  seqfeq3  10790  seqfeq4g  10792  expaddzaplem  10843  expaddzap  10844  expmulzap  10846  zesq  10919  bcm1k  11021  bccl  11028  permnn  11032  seq3coll  11105  ccatrn  11185  shftuz  11377  ref  11415  imf  11416  crre  11417  rereb  11423  resqrexlemnm  11578  absf  11670  summodclem2a  11941  summodc  11943  fsumgcl  11946  fsum3  11947  fsumf1o  11950  fsumcnv  11997  mptfzshft  12002  isumlessdc  12056  geolim2  12072  prodmodclem3  12135  fprodseq  12143  fprodf1o  12148  dvdsaddre2b  12401  3dvds  12424  oexpneg  12437  nn0ob  12468  divalglemqt  12479  gcdf  12542  lcmgcdlem  12648  sqnprm  12707  sqrt2irrlem  12732  2sqpwodd  12747  fnum  12761  fden  12762  phimullem  12796  pc2dvds  12902  gzsubcl  12952  4sqlem5  12954  4sqlem9  12958  4sqlem10  12959  mul4sqlem  12965  mul4sq  12966  4sqlem11  12973  4sqlem13m  12975  4sqlem16  12978  4sqlem17  12979  4sqlem18  12980  ctiunctlemfo  13059  ptex  13346  prdsval  13355  prdsbas  13358  prdsbascl  13371  mgmsscl  13443  subsubm  13565  mhmima  13573  imasgrp2  13696  mhmmnd  13702  mulgdir  13740  subgmulg  13774  issubg2m  13775  issubgrpd2  13776  grpissubg  13780  subsubg  13783  isnsg3  13793  ssnmz  13797  eqger  13810  eqgen  13813  ecqusaddcl  13825  ghmrn  13843  ghmnsgima  13854  conjsubg  13863  conjnmz  13865  ring1  14071  dvdsrvald  14106  dvdsrd  14107  dvdsrex  14111  0unit  14142  invrpropdg  14162  lringuplu  14209  subrngin  14226  subsubrng  14227  subrgcrng  14238  subrgin  14257  subsubrg  14258  islmodd  14306  lssvacl  14378  lssvancl1  14380  lss0cl  14382  lssvscl  14388  lssvnegcl  14389  lssincl  14398  issubrgd  14465  lidlrsppropdg  14508  2idlcpblrng  14536  zsssubrg  14598  unopn  14728  tsettps  14761  tgss2  14802  difopn  14831  resttop  14893  resttopon  14894  restco  14897  tgcn  14931  tgcnp  14932  cnptopco  14945  upxp  14995  txcn  14998  txdis  15000  cnmpt11  15006  cnmpt11f  15007  cnmpt1t  15008  cnmpt12  15010  cnmpt21  15014  cnmpt21f  15015  cnmpt2t  15016  cnmpt22  15017  cnmpt22f  15018  cnmpt1res  15019  xmeter  15159  mscl  15188  xmscl  15189  bdxmet  15224  cncfmpt1f  15321  cdivcncfap  15327  negfcncf  15329  ivthreinc  15368  cnmptlimc  15397  dvcnp2cntop  15422  elplyd  15464  plypow  15467  plyconst  15468  plyaddlem1  15470  plysub  15476  dvply2g  15489  sincn  15492  coscn  15493  relogcl  15585  mpodvdsmulf1o  15713  fsumdvdsmul  15714  mersenne  15720  perfect  15724  lgsne0  15766  lgseisenlem4  15801  lgsquadlem1  15805  usgr1vr  16098  p1evtxdeqfilem  16161  isclwwlkn  16263  clwwlknon  16279  pwtrufal  16598