Theorem eqeltrrd 2310

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  3eltr3d  2315  exmid01  4311  pwntru  4312  xpexr2m  5204  funimaexg  5440  fndmexd  5556  fvmptdv2  5767  ffvresb  5840  iotaexel  6008  2ndrn  6377  1st2ndbr  6378  elopabi  6391  cnvf1olem  6420  dftpos4  6494  tfrlemibxssdm  6558  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  nnmordi  6749  th3qlem1  6871  infiexmid  7134  onunsnss  7177  ssfirab  7197  ssfidc  7198  fnfi  7203  fidcenumlemr  7225  elfi2  7259  ordiso2  7326  djulclb  7346  ctmlemr  7399  ctssdccl  7402  ctssdc  7404  exmidfodomrlemreseldju  7503  exmidfodomrlemr  7505  pw1m  7534  exmidapne  7574  archnqq  7732  prarloclemarch2  7734  enq0tr  7749  nqnq0  7756  addcmpblnq0  7758  mulcmpblnq0  7759  mulcanenq0ec  7760  addclnq0  7766  mulclnq0  7767  nqpnq0nq  7768  nq0m0r  7771  distrnq0  7774  addassnq0lemcl  7776  prarloclemlt  7808  prarloclem5  7815  distrlem4prl  7899  distrlem4pru  7900  ltexprlemm  7915  ltexprlemrl  7925  ltexprlemru  7927  addcanprleml  7929  cauappcvgprlemladdru  7971  prsrlem1  8057  mulgt0sr  8093  axpre-suploclemres  8216  cnegexlem2  8449  subf  8475  resubcl  8537  negcon1ad  8579  subeq0bd  8652  rimul  8859  rereim  8860  aprcl  8920  nn0nnaddcl  9527  elnn0nn  9538  zaddcllemneg  9616  zsubcl  9618  zrevaddcl  9628  elz2  9649  zdiv  9666  peano5uzti  9686  peano2uzr  9917  uzaddcl  9918  divfnzn  9953  qsubcl  9970  qrevaddcl  9976  fseq1p1m1  10428  suprzubdc  10596  modqmuladdim  10729  frec2uzrand  10767  frecuzrdglem  10773  frecuzrdg0  10775  frecuzrdgdomlem  10779  frecuzrdg0t  10784  frecuzrdgsuctlem  10785  seq3val  10822  seq3feq  10842  iseqf1olemnab  10863  seqf1oglem2  10882  seqfeq3  10891  seqfeq4g  10893  expaddzaplem  10944  expaddzap  10945  expmulzap  10947  zesq  11020  bcm1k  11122  bccl  11129  permnn  11134  seq3coll  11214  ccatrn  11297  shftuz  11502  ref  11540  imf  11541  crre  11542  rereb  11548  resqrexlemnm  11703  absf  11795  summodclem2a  12067  summodc  12069  fsumgcl  12072  fsum3  12073  fsumf1o  12076  fsumcnv  12123  mptfzshft  12128  isumlessdc  12182  geolim2  12198  prodmodclem3  12261  fprodseq  12269  fprodf1o  12274  dvdsaddre2b  12527  3dvds  12550  oexpneg  12563  nn0ob  12594  divalglemqt  12605  gcdf  12668  lcmgcdlem  12774  sqnprm  12833  sqrt2irrlem  12858  2sqpwodd  12873  fnum  12887  fden  12888  phimullem  12922  pc2dvds  13028  gzsubcl  13078  4sqlem5  13080  4sqlem9  13084  4sqlem10  13085  mul4sqlem  13091  mul4sq  13092  4sqlem11  13099  4sqlem13m  13101  4sqlem16  13104  4sqlem17  13105  4sqlem18  13106  ballotfilem2  13142  ctiunctlemfo  13190  ptex  13477  prdsval  13486  prdsbas  13489  prdsbascl  13502  mgmsscl  13574  subsubm  13696  mhmima  13704  imasgrp2  13827  mhmmnd  13833  mulgdir  13871  subgmulg  13905  issubg2m  13906  issubgrpd2  13907  grpissubg  13911  subsubg  13914  isnsg3  13924  ssnmz  13928  eqger  13941  eqgen  13944  ecqusaddcl  13956  ghmrn  13974  ghmnsgima  13985  conjsubg  13994  conjnmz  13996  ring1  14203  dvdsrvald  14238  dvdsrd  14239  dvdsrex  14243  0unit  14274  invrpropdg  14294  lringuplu  14341  subrngin  14358  subsubrng  14359  subrgcrng  14370  subrgin  14389  subsubrg  14390  aprnzr  14433  aprlring  14434  islmodd  14441  lssvacl  14513  lssvancl1  14515  lss0cl  14517  lssvscl  14523  lssvnegcl  14524  lssincl  14533  issubrgd  14600  lidlrsppropdg  14643  2idlcpblrng  14671  zsssubrg  14733  unopn  14870  tsettps  14903  tgss2  14944  difopn  14973  resttop  15035  resttopon  15036  restco  15039  tgcn  15073  tgcnp  15074  cnptopco  15087  upxp  15137  txcn  15140  txdis  15142  cnmpt11  15148  cnmpt11f  15149  cnmpt1t  15150  cnmpt12  15152  cnmpt21  15156  cnmpt21f  15157  cnmpt2t  15158  cnmpt22  15159  cnmpt22f  15160  cnmpt1res  15161  xmeter  15301  mscl  15330  xmscl  15331  bdxmet  15366  cncfmpt1f  15463  cdivcncfap  15469  negfcncf  15471  ivthreinc  15510  cnmptlimc  15539  dvcnp2cntop  15564  elplyd  15606  plypow  15609  plyconst  15610  plyaddlem1  15612  plysub  15618  dvply2g  15631  sincn  15634  coscn  15635  relogcl  15727  mpodvdsmulf1o  15858  fsumdvdsmul  15859  mersenne  15865  perfect  15869  lgsne0  15911  lgseisenlem4  15946  lgsquadlem1  15950  usgr1vr  16243  p1evtxdeqfilem  16306  isclwwlkn  16408  clwwlknon  16424  pwtrufal  16771  repiecele0  16810  qdiff  16833  gfsumcl  16870