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 ⊢ (𝜑 → 𝐵 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced by:  3eltr3d  2321  exmid01  4330  pwntru  4331  xpexr2m  5224  funimaexg  5460  fndmexd  5576  fvmptdv2  5789  ffvresb  5862  iotaexel  6033  2ndrn  6407  1st2ndbr  6408  elopabi  6421  cnvf1olem  6450  dftpos4  6524  tfrlemibxssdm  6588  tfr1onlembxssdm  6604  tfrcllembxssdm  6617  nnmordi  6779  th3qlem1  6901  infiexmid  7171  onunsnss  7214  ssfirab  7234  ssfidc  7235  fnfi  7240  fidcenumlemr  7262  elfi2  7296  f1setfi  7307  ordiso2  7365  djulclb  7385  ctmlemr  7438  ctssdccl  7441  ctssdc  7443  exmidfodomrlemreseldju  7542  exmidfodomrlemr  7544  pw1m  7573  exmidapne  7616  archnqq  7774  prarloclemarch2  7776  enq0tr  7791  nqnq0  7798  addcmpblnq0  7800  mulcmpblnq0  7801  mulcanenq0ec  7802  addclnq0  7808  mulclnq0  7809  nqpnq0nq  7810  nq0m0r  7813  distrnq0  7816  addassnq0lemcl  7818  prarloclemlt  7850  prarloclem5  7857  distrlem4prl  7941  distrlem4pru  7942  ltexprlemm  7957  ltexprlemrl  7967  ltexprlemru  7969  addcanprleml  7971  cauappcvgprlemladdru  8013  prsrlem1  8099  mulgt0sr  8135  axpre-suploclemres  8258  cnegexlem2  8492  subf  8518  resubcl  8580  negcon1ad  8622  subeq0bd  8696  rimul  8903  rereim  8904  aprcl  8964  nn0nnaddcl  9573  elnn0nn  9584  zaddcllemneg  9662  zsubcl  9664  zrevaddcl  9674  elz2  9695  zdiv  9713  peano5uzti  9733  peano2uzr  9964  uzaddcl  9965  divfnzn  10000  qsubcl  10017  qrevaddcl  10023  fseq1p1m1  10479  suprzubdc  10649  modqmuladdim  10782  frec2uzrand  10820  frecuzrdglem  10826  frecuzrdg0  10828  frecuzrdgdomlem  10832  frecuzrdg0t  10837  frecuzrdgsuctlem  10838  seq3val  10875  seq3feq  10895  iseqf1olemnab  10916  seqf1oglem2  10935  seqfeq3  10944  seqfeq4g  10946  expaddzaplem  10997  expaddzap  10998  expmulzap  11000  zesq  11074  bcm1k  11176  bccl  11183  permnn  11188  hashf1lem2  11264  hashf1  11265  seq3coll  11272  ccatrn  11355  shftuz  11560  ref  11598  imf  11599  crre  11600  rereb  11606  resqrexlemnm  11762  absf  11854  summodclem2a  12126  summodc  12128  fsumgcl  12131  fsum3  12132  fsumf1o  12135  fsumcnv  12182  mptfzshft  12187  isumlessdc  12241  geolim2  12257  prodmodclem3  12320  fprodseq  12328  fprodf1o  12333  dvdsaddre2b  12586  3dvds  12609  oexpneg  12622  nn0ob  12653  divalglemqt  12664  gcdf  12727  lcmgcdlem  12833  sqnprm  12892  sqrt2irrlem  12917  2sqpwodd  12932  fnum  12946  fden  12947  phimullem  12981  pc2dvds  13087  gzsubcl  13137  4sqlem5  13139  4sqlem9  13143  4sqlem10  13144  mul4sqlem  13150  mul4sq  13151  4sqlem11  13158  4sqlem13m  13160  4sqlem16  13163  4sqlem17  13164  4sqlem18  13165  ballotfilem2  13206  ballotfilemsf1o  13235  ballotfilemrinv0  13254  ctiunctlemfo  13308  ptex  13595  mgmsscl  13658  subsubm  13767  mhmima  13775  imasgrp2  13890  mhmmnd  13896  mulgdir  13934  subgmulg  13968  issubg2m  13969  issubgrpd2  13970  grpissubg  13974  subsubg  13977  isnsg3  13987  ssnmz  13991  eqger  14004  eqgen  14007  ecqusaddcl  14019  ghmrn  14037  ghmnsgima  14048  conjsubg  14057  conjnmz  14059  gsumclfi  14136  gsumsubmclfi  14140  prdsval  14150  prdsbas  14153  prdsbascl  14166  ring1  14337  dvdsrvald  14373  dvdsrd  14374  dvdsrex  14378  0unit  14409  invrpropdg  14429  lringuplu  14476  subrngin  14494  subsubrng  14495  subrgcrng  14506  subrgin  14525  subsubrg  14526  aprnzr  14572  aprlring  14573  islmodd  14602  lssvacl  14674  lssvancl1  14676  lss0cl  14678  lssvscl  14684  lssvnegcl  14685  lssincl  14694  issubrgd  14761  lidlrsppropdg  14804  2idlcpblrng  14832  zsssubrg  14894  unopn  15029  tsettps  15062  tgss2  15103  difopn  15132  resttop  15194  resttopon  15195  restco  15198  tgcn  15232  tgcnp  15233  cnptopco  15246  upxp  15296  txcn  15299  txdis  15301  cnmpt11  15307  cnmpt11f  15308  cnmpt1t  15309  cnmpt12  15311  cnmpt21  15315  cnmpt21f  15316  cnmpt2t  15317  cnmpt22  15318  cnmpt22f  15319  cnmpt1res  15320  xmeter  15460  mscl  15489  xmscl  15490  bdxmet  15525  cncfmpt1f  15622  cdivcncfap  15628  negfcncf  15630  ivthreinc  15669  cnmptlimc  15698  dvcnp2cntop  15723  elplyd  15765  plypow  15768  plyconst  15769  plyaddlem1  15771  plysub  15777  dvply2g  15790  sincn  15793  coscn  15794  relogcl  15886  mpodvdsmulf1o  16018  fsumdvdsmul  16019  mersenne  16025  perfect  16029  lgsne0  16071  lgseisenlem4  16106  lgsquadlem1  16110  usgr1vr  16403  p1evtxdeqfilem  16466  isclwwlkn  16568  clwwlknon  16584  pwtrufal  16941  repiecele0  16980  qdiff  17003