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 1398   ∈ 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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  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  4294  pwntru  4295  xpexr2m  5185  funimaexg  5421  fndmexd  5534  fvmptdv2  5745  ffvresb  5818  iotaexel  5986  2ndrn  6355  1st2ndbr  6356  elopabi  6369  cnvf1olem  6398  dftpos4  6472  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  nnmordi  6727  th3qlem1  6849  infiexmid  7109  onunsnss  7152  ssfirab  7172  ssfidc  7173  fnfi  7178  fidcenumlemr  7197  elfi2  7231  ordiso2  7294  djulclb  7314  ctmlemr  7367  ctssdccl  7370  ctssdc  7372  exmidfodomrlemreseldju  7471  exmidfodomrlemr  7473  pw1m  7502  exmidapne  7539  archnqq  7697  prarloclemarch2  7699  enq0tr  7714  nqnq0  7721  addcmpblnq0  7723  mulcmpblnq0  7724  mulcanenq0ec  7725  addclnq0  7731  mulclnq0  7732  nqpnq0nq  7733  nq0m0r  7736  distrnq0  7739  addassnq0lemcl  7741  prarloclemlt  7773  prarloclem5  7780  distrlem4prl  7864  distrlem4pru  7865  ltexprlemm  7880  ltexprlemrl  7890  ltexprlemru  7892  addcanprleml  7894  cauappcvgprlemladdru  7936  prsrlem1  8022  mulgt0sr  8058  axpre-suploclemres  8181  cnegexlem2  8414  subf  8440  resubcl  8502  negcon1ad  8544  subeq0bd  8617  rimul  8824  rereim  8825  aprcl  8885  nn0nnaddcl  9492  elnn0nn  9503  zaddcllemneg  9579  zsubcl  9581  zrevaddcl  9591  elz2  9612  zdiv  9629  peano5uzti  9649  peano2uzr  9880  uzaddcl  9881  divfnzn  9916  qsubcl  9933  qrevaddcl  9939  fseq1p1m1  10391  suprzubdc  10559  modqmuladdim  10692  frec2uzrand  10730  frecuzrdglem  10736  frecuzrdg0  10738  frecuzrdgdomlem  10742  frecuzrdg0t  10747  frecuzrdgsuctlem  10748  seq3val  10785  seq3feq  10805  iseqf1olemnab  10826  seqf1oglem2  10845  seqfeq3  10854  seqfeq4g  10856  expaddzaplem  10907  expaddzap  10908  expmulzap  10910  zesq  10983  bcm1k  11085  bccl  11092  permnn  11096  seq3coll  11169  ccatrn  11252  shftuz  11457  ref  11495  imf  11496  crre  11497  rereb  11503  resqrexlemnm  11658  absf  11750  summodclem2a  12022  summodc  12024  fsumgcl  12027  fsum3  12028  fsumf1o  12031  fsumcnv  12078  mptfzshft  12083  isumlessdc  12137  geolim2  12153  prodmodclem3  12216  fprodseq  12224  fprodf1o  12229  dvdsaddre2b  12482  3dvds  12505  oexpneg  12518  nn0ob  12549  divalglemqt  12560  gcdf  12623  lcmgcdlem  12729  sqnprm  12788  sqrt2irrlem  12813  2sqpwodd  12828  fnum  12842  fden  12843  phimullem  12877  pc2dvds  12983  gzsubcl  13033  4sqlem5  13035  4sqlem9  13039  4sqlem10  13040  mul4sqlem  13046  mul4sq  13047  4sqlem11  13054  4sqlem13m  13056  4sqlem16  13059  4sqlem17  13060  4sqlem18  13061  ctiunctlemfo  13140  ptex  13427  prdsval  13436  prdsbas  13439  prdsbascl  13452  mgmsscl  13524  subsubm  13646  mhmima  13654  imasgrp2  13777  mhmmnd  13783  mulgdir  13821  subgmulg  13855  issubg2m  13856  issubgrpd2  13857  grpissubg  13861  subsubg  13864  isnsg3  13874  ssnmz  13878  eqger  13891  eqgen  13894  ecqusaddcl  13906  ghmrn  13924  ghmnsgima  13935  conjsubg  13944  conjnmz  13946  ring1  14153  dvdsrvald  14188  dvdsrd  14189  dvdsrex  14193  0unit  14224  invrpropdg  14244  lringuplu  14291  subrngin  14308  subsubrng  14309  subrgcrng  14320  subrgin  14339  subsubrg  14340  islmodd  14389  lssvacl  14461  lssvancl1  14463  lss0cl  14465  lssvscl  14471  lssvnegcl  14472  lssincl  14481  issubrgd  14548  lidlrsppropdg  14591  2idlcpblrng  14619  zsssubrg  14681  unopn  14816  tsettps  14849  tgss2  14890  difopn  14919  resttop  14981  resttopon  14982  restco  14985  tgcn  15019  tgcnp  15020  cnptopco  15033  upxp  15083  txcn  15086  txdis  15088  cnmpt11  15094  cnmpt11f  15095  cnmpt1t  15096  cnmpt12  15098  cnmpt21  15102  cnmpt21f  15103  cnmpt2t  15104  cnmpt22  15105  cnmpt22f  15106  cnmpt1res  15107  xmeter  15247  mscl  15276  xmscl  15277  bdxmet  15312  cncfmpt1f  15409  cdivcncfap  15415  negfcncf  15417  ivthreinc  15456  cnmptlimc  15485  dvcnp2cntop  15510  elplyd  15552  plypow  15555  plyconst  15556  plyaddlem1  15558  plysub  15564  dvply2g  15577  sincn  15580  coscn  15581  relogcl  15673  mpodvdsmulf1o  15804  fsumdvdsmul  15805  mersenne  15811  perfect  15815  lgsne0  15857  lgseisenlem4  15892  lgsquadlem1  15896  usgr1vr  16189  p1evtxdeqfilem  16252  isclwwlkn  16354  clwwlknon  16370  pwtrufal  16719  repiecele0  16758  qdiff  16781  gfsumcl  16816