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  6699  erth  6734  ecelqsdm  6760  phpm  7035  exmidpweq  7082  pw1if  7421  cc2lem  7463  cc3  7465  suplocexprlemmu  7916  suplocexprlemloc  7919  lincmb01cmp  10211  fzopth  10269  fzoaddel2  10408  fzosubel2  10413  fzocatel  10417  zpnn0elfzo1  10426  fzoend  10440  peano2fzor  10450  monoord2  10720  ser3mono  10721  bcpasc  11000  zfz1isolemiso  11074  swrdclg  11198  fisum0diag2  11974  isumsplit  12018  prodmodclem3  12102  prodmodclem2a  12103  nnmindc  12571  nnminle  12572  bassetsnn  13105  basmexd  13109  basm  13110  prdsbasfn  13330  prdsbasprj  13331  pwsplusgval  13344  pwsmulrval  13345  mgm1  13419  grpidd  13432  gsumress  13444  sgrppropd  13462  ismndd  13486  mndpropd  13489  issubmnd  13491  imasmnd  13502  grpidd2  13590  pwsinvg  13661  imasgrp  13664  submmulg  13719  subginvcl  13736  subgcl  13737  subgsub  13739  subgmulg  13741  1nsgtrivd  13772  quseccl0g  13784  kerf1ghm  13827  rngass  13918  rngcl  13923  rngpropd  13934  imasrng  13935  srgcl  13949  srgass  13950  srg1zr  13966  srgpcomp  13969  srgpcompp  13970  srgpcomppsc  13971  crngcom  13993  ringass  13995  ringidmlem  14001  ringidss  14008  ringpropd  14017  imasring  14043  qusring2  14045  mulgass3  14064  dvdsrd  14074  1unit  14087  unitmulcl  14093  dvrvald  14114  rdivmuldivd  14124  elrhmunit  14157  rhmunitinv  14158  lringuplu  14176  subrngmcl  14189  subrg1  14211  subrgmcl  14213  subrgdv  14218  subrgunit  14219  resrhm  14228  aprval  14262  aprirr  14263  aprsym  14264  aprcotr  14265  lmodprop2d  14328  lidlss  14456  lidl0cl  14463  lidlacl  14464  lidlnegcl  14465  rnglidlmsgrp  14477  2idllidld  14486  2idlridld  14487  2idlcpblrng  14503  qus1  14506  quscrng  14513  rspsn  14514  znf1o  14631  psrbagfi  14653  psrelbas  14655  iscnp4  14908  cnrest2r  14927  txbasval  14957  txlm  14969  xmetunirn  15048  xblss2ps  15094  blbas  15123  mopntopon  15133  isxms2  15142  metcnpi  15205  metcnpi2  15206  tgioo  15244  cncfmpt2fcntop  15289  limccl  15349  limcimolemlt  15354  limccnp2cntop  15367  dvmulxxbr  15392  dvcoapbr  15397  dvcjbr  15398  dvrecap  15403  plyaddlem1  15437  plymullem1  15438  plycoeid3  15447  lgseisenlem4  15768  clwwlkccatlem  16143