Theorem eleqtrd 2313

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 2304	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

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

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 2216

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

This theorem is referenced by:  eleqtrrd  2314  3eltr3d  2317  eleqtrid  2323  eleqtrdi  2327  opth1  4357  0nelop  4369  tfisi  4714  nnpredlt  4751  iotam  5349  ercl  6791  erth  6826  ecelqsdm  6852  phpm  7133  exmidpweq  7182  pw1if  7548  cc2lem  7596  cc3  7598  suplocexprlemmu  8049  suplocexprlemloc  8052  lincmb01cmp  10355  fzopth  10416  fzoaddel2  10557  fzosubel2  10562  fzocatel  10566  zpnn0elfzo1  10575  fzoend  10589  peano2fzor  10599  infssfzcldc  10618  infssfzledc  10619  monoord2  10872  ser3mono  10873  bcpasc  11153  zfz1isolemiso  11236  swrdclg  11367  fisum0diag2  12158  isumsplit  12202  prodmodclem3  12286  prodmodclem2a  12287  nnmindc  12755  nnminle  12756  bassetsnn  13353  basmexd  13357  basm  13358  mgm1  13633  grpidd  13646  gsumress  13658  sgrppropd  13676  ismndd  13698  mndpropd  13701  issubmnd  13703  imasmnd  13708  grpidd2  13796  imasgrp  13864  submmulg  13919  subginvcl  13936  subgcl  13937  subgsub  13939  subgmulg  13941  1nsgtrivd  13972  quseccl0g  13984  kerf1ghm  14027  prdsbasfn  14123  prdsbasprj  14124  pwsplusgval  14150  pwsmulrval  14151  pwsinvg  14157  rngass  14178  rngcl  14183  rngpropd  14194  imasrng  14195  srgcl  14213  srgass  14214  srgpcomp  14233  srgpcompp  14234  srgpcomppsc  14235  crngcom  14257  ringass  14259  ringidmlem  14265  ringidss  14272  ringpropd  14281  imasring  14307  qusring2  14309  mulgass3  14329  dvdsrd  14339  1unit  14352  unitmulcl  14358  dvrvald  14379  rdivmuldivd  14389  elrhmunit  14422  rhmunitinv  14423  lringuplu  14441  subrngmcl  14455  subrg1  14477  subrgmcl  14479  subrgdv  14484  subrgunit  14485  resrhm  14494  aprval  14529  aprirr  14533  aprsym  14534  aprcotr  14535  opprdrng  14558  lmodprop2d  14622  lidlss  14750  lidl0cl  14757  lidlacl  14758  lidlnegcl  14759  rnglidlmsgrp  14771  2idllidld  14780  2idlridld  14781  2idlcpblrng  14797  qus1  14800  quscrng  14807  rspsn  14808  znf1o  14925  psrbagfi  14949  psrelbas  14956  iscnp4  15209  cnrest2r  15228  txbasval  15258  txlm  15270  xmetunirn  15349  xblss2ps  15395  blbas  15424  mopntopon  15434  isxms2  15443  metcnpi  15506  metcnpi2  15507  tgioo  15545  cncfmpt2fcntop  15590  limccl  15650  limcimolemlt  15655  limccnp2cntop  15668  dvmulxxbr  15693  dvcoapbr  15698  dvcjbr  15699  dvrecap  15704  plyaddlem1  15738  plymullem1  15739  plycoeid3  15748  lgseisenlem4  16072  usgr1vr  16369  clwwlkccatlem  16521