Theorem eleqtrd 2284

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleqtrrd  2285  3eltr3d  2288  eleqtrid  2294  eleqtrdi  2298  opth1  4280  0nelop  4292  tfisi  4635  nnpredlt  4672  iotam  5263  ercl  6631  erth  6666  ecelqsdm  6692  phpm  6962  exmidpweq  7006  cc2lem  7378  cc3  7380  suplocexprlemmu  7831  suplocexprlemloc  7834  lincmb01cmp  10125  fzopth  10183  fzoaddel2  10319  fzosubel2  10324  fzocatel  10328  zpnn0elfzo1  10337  fzoend  10351  peano2fzor  10361  monoord2  10631  ser3mono  10632  bcpasc  10911  zfz1isolemiso  10984  swrdclg  11103  fisum0diag2  11758  isumsplit  11802  prodmodclem3  11886  prodmodclem2a  11887  nnmindc  12355  nnminle  12356  basmexd  12892  basm  12893  prdsbasfn  13113  prdsbasprj  13114  pwsplusgval  13127  pwsmulrval  13128  mgm1  13202  grpidd  13215  gsumress  13227  sgrppropd  13245  ismndd  13269  mndpropd  13272  issubmnd  13274  imasmnd  13285  grpidd2  13373  pwsinvg  13444  imasgrp  13447  submmulg  13502  subginvcl  13519  subgcl  13520  subgsub  13522  subgmulg  13524  1nsgtrivd  13555  quseccl0g  13567  kerf1ghm  13610  rngass  13701  rngcl  13706  rngpropd  13717  imasrng  13718  srgcl  13732  srgass  13733  srg1zr  13749  srgpcomp  13752  srgpcompp  13753  srgpcomppsc  13754  crngcom  13776  ringass  13778  ringidmlem  13784  ringidss  13791  ringpropd  13800  imasring  13826  qusring2  13828  mulgass3  13847  dvdsrd  13856  1unit  13869  unitmulcl  13875  dvrvald  13896  rdivmuldivd  13906  elrhmunit  13939  rhmunitinv  13940  lringuplu  13958  subrngmcl  13971  subrg1  13993  subrgmcl  13995  subrgdv  14000  subrgunit  14001  resrhm  14010  aprval  14044  aprirr  14045  aprsym  14046  aprcotr  14047  lmodprop2d  14110  lidlss  14238  lidl0cl  14245  lidlacl  14246  lidlnegcl  14247  rnglidlmsgrp  14259  2idllidld  14268  2idlridld  14269  2idlcpblrng  14285  qus1  14288  quscrng  14295  rspsn  14296  znf1o  14413  psrbagfi  14435  psrelbas  14437  iscnp4  14690  cnrest2r  14709  txbasval  14739  txlm  14751  xmetunirn  14830  xblss2ps  14876  blbas  14905  mopntopon  14915  isxms2  14924  metcnpi  14987  metcnpi2  14988  tgioo  15026  cncfmpt2fcntop  15071  limccl  15131  limcimolemlt  15136  limccnp2cntop  15149  dvmulxxbr  15174  dvcoapbr  15179  dvcjbr  15180  dvrecap  15185  plyaddlem1  15219  plymullem1  15220  plycoeid3  15229  lgseisenlem4  15550