Theorem eleqtrd 2308

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eleqtrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	eleq2d 2299	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

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

This theorem is referenced by:  eleqtrrd  2309  3eltr3d  2312  eleqtrid  2318  eleqtrdi  2322  opth1  4322  0nelop  4334  tfisi  4679  nnpredlt  4716  iotam  5310  ercl  6691  erth  6726  ecelqsdm  6752  phpm  7027  exmidpweq  7071  pw1if  7410  cc2lem  7452  cc3  7454  suplocexprlemmu  7905  suplocexprlemloc  7908  lincmb01cmp  10199  fzopth  10257  fzoaddel2  10396  fzosubel2  10401  fzocatel  10405  zpnn0elfzo1  10414  fzoend  10428  peano2fzor  10438  monoord2  10708  ser3mono  10709  bcpasc  10988  zfz1isolemiso  11061  swrdclg  11182  fisum0diag2  11958  isumsplit  12002  prodmodclem3  12086  prodmodclem2a  12087  nnmindc  12555  nnminle  12556  bassetsnn  13089  basmexd  13093  basm  13094  prdsbasfn  13314  prdsbasprj  13315  pwsplusgval  13328  pwsmulrval  13329  mgm1  13403  grpidd  13416  gsumress  13428  sgrppropd  13446  ismndd  13470  mndpropd  13473  issubmnd  13475  imasmnd  13486  grpidd2  13574  pwsinvg  13645  imasgrp  13648  submmulg  13703  subginvcl  13720  subgcl  13721  subgsub  13723  subgmulg  13725  1nsgtrivd  13756  quseccl0g  13768  kerf1ghm  13811  rngass  13902  rngcl  13907  rngpropd  13918  imasrng  13919  srgcl  13933  srgass  13934  srg1zr  13950  srgpcomp  13953  srgpcompp  13954  srgpcomppsc  13955  crngcom  13977  ringass  13979  ringidmlem  13985  ringidss  13992  ringpropd  14001  imasring  14027  qusring2  14029  mulgass3  14048  dvdsrd  14058  1unit  14071  unitmulcl  14077  dvrvald  14098  rdivmuldivd  14108  elrhmunit  14141  rhmunitinv  14142  lringuplu  14160  subrngmcl  14173  subrg1  14195  subrgmcl  14197  subrgdv  14202  subrgunit  14203  resrhm  14212  aprval  14246  aprirr  14247  aprsym  14248  aprcotr  14249  lmodprop2d  14312  lidlss  14440  lidl0cl  14447  lidlacl  14448  lidlnegcl  14449  rnglidlmsgrp  14461  2idllidld  14470  2idlridld  14471  2idlcpblrng  14487  qus1  14490  quscrng  14497  rspsn  14498  znf1o  14615  psrbagfi  14637  psrelbas  14639  iscnp4  14892  cnrest2r  14911  txbasval  14941  txlm  14953  xmetunirn  15032  xblss2ps  15078  blbas  15107  mopntopon  15117  isxms2  15126  metcnpi  15189  metcnpi2  15190  tgioo  15228  cncfmpt2fcntop  15273  limccl  15333  limcimolemlt  15338  limccnp2cntop  15351  dvmulxxbr  15376  dvcoapbr  15381  dvcjbr  15382  dvrecap  15387  plyaddlem1  15421  plymullem1  15422  plycoeid3  15431  lgseisenlem4  15752