Theorem eleqtrd 2310

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 2301	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 147	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:  eleqtrrd  2311  3eltr3d  2314  eleqtrid  2320  eleqtrdi  2324  opth1  4334  0nelop  4346  tfisi  4691  nnpredlt  4728  iotam  5325  ercl  6756  erth  6791  ecelqsdm  6817  phpm  7095  exmidpweq  7144  pw1if  7503  cc2lem  7545  cc3  7547  suplocexprlemmu  7998  suplocexprlemloc  8001  lincmb01cmp  10299  fzopth  10358  fzoaddel2  10498  fzosubel2  10503  fzocatel  10507  zpnn0elfzo1  10516  fzoend  10530  peano2fzor  10540  monoord2  10811  ser3mono  10812  bcpasc  11091  zfz1isolemiso  11166  swrdclg  11297  fisum0diag2  12088  isumsplit  12132  prodmodclem3  12216  prodmodclem2a  12217  nnmindc  12685  nnminle  12686  bassetsnn  13219  basmexd  13223  basm  13224  prdsbasfn  13444  prdsbasprj  13445  pwsplusgval  13458  pwsmulrval  13459  mgm1  13533  grpidd  13546  gsumress  13558  sgrppropd  13576  ismndd  13600  mndpropd  13603  issubmnd  13605  imasmnd  13616  grpidd2  13704  pwsinvg  13775  imasgrp  13778  submmulg  13833  subginvcl  13850  subgcl  13851  subgsub  13853  subgmulg  13855  1nsgtrivd  13886  quseccl0g  13898  kerf1ghm  13941  rngass  14033  rngcl  14038  rngpropd  14049  imasrng  14050  srgcl  14064  srgass  14065  srg1zr  14081  srgpcomp  14084  srgpcompp  14085  srgpcomppsc  14086  crngcom  14108  ringass  14110  ringidmlem  14116  ringidss  14123  ringpropd  14132  imasring  14158  qusring2  14160  mulgass3  14179  dvdsrd  14189  1unit  14202  unitmulcl  14208  dvrvald  14229  rdivmuldivd  14239  elrhmunit  14272  rhmunitinv  14273  lringuplu  14291  subrngmcl  14304  subrg1  14326  subrgmcl  14328  subrgdv  14333  subrgunit  14334  resrhm  14343  aprval  14378  aprirr  14379  aprsym  14380  aprcotr  14381  lmodprop2d  14444  lidlss  14572  lidl0cl  14579  lidlacl  14580  lidlnegcl  14581  rnglidlmsgrp  14593  2idllidld  14602  2idlridld  14603  2idlcpblrng  14619  qus1  14622  quscrng  14629  rspsn  14630  znf1o  14747  psrbagfi  14770  psrelbas  14776  iscnp4  15029  cnrest2r  15048  txbasval  15078  txlm  15090  xmetunirn  15169  xblss2ps  15215  blbas  15244  mopntopon  15254  isxms2  15263  metcnpi  15326  metcnpi2  15327  tgioo  15365  cncfmpt2fcntop  15410  limccl  15470  limcimolemlt  15475  limccnp2cntop  15488  dvmulxxbr  15513  dvcoapbr  15518  dvcjbr  15519  dvrecap  15524  plyaddlem1  15558  plymullem1  15559  plycoeid3  15568  lgseisenlem4  15892  usgr1vr  16189  clwwlkccatlem  16341