Theorem eleqtrd 2275

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eleqtrrd  2276  3eltr3d  2279  eleqtrid  2285  eleqtrdi  2289  opth1  4269  0nelop  4281  tfisi  4623  nnpredlt  4660  iotam  5250  ercl  6603  erth  6638  ecelqsdm  6664  phpm  6926  exmidpweq  6970  cc2lem  7333  cc3  7335  suplocexprlemmu  7785  suplocexprlemloc  7788  lincmb01cmp  10078  fzopth  10136  fzoaddel2  10269  fzosubel2  10271  fzocatel  10275  zpnn0elfzo1  10284  fzoend  10298  peano2fzor  10308  monoord2  10578  ser3mono  10579  bcpasc  10858  zfz1isolemiso  10931  fisum0diag2  11612  isumsplit  11656  prodmodclem3  11740  prodmodclem2a  11741  nnmindc  12201  nnminle  12202  basmexd  12738  basm  12739  mgm1  13013  grpidd  13026  gsumress  13038  sgrppropd  13056  ismndd  13078  mndpropd  13081  issubmnd  13083  grpidd2  13173  imasgrp  13241  submmulg  13296  subginvcl  13313  subgcl  13314  subgsub  13316  subgmulg  13318  1nsgtrivd  13349  quseccl0g  13361  kerf1ghm  13404  rngass  13495  rngcl  13500  rngpropd  13511  imasrng  13512  srgcl  13526  srgass  13527  srg1zr  13543  srgpcomp  13546  srgpcompp  13547  srgpcomppsc  13548  crngcom  13570  ringass  13572  ringidmlem  13578  ringidss  13585  ringpropd  13594  imasring  13620  qusring2  13622  mulgass3  13641  dvdsrd  13650  1unit  13663  unitmulcl  13669  dvrvald  13690  rdivmuldivd  13700  elrhmunit  13733  rhmunitinv  13734  lringuplu  13752  subrngmcl  13765  subrg1  13787  subrgmcl  13789  subrgdv  13794  subrgunit  13795  resrhm  13804  aprval  13838  aprirr  13839  aprsym  13840  aprcotr  13841  lmodprop2d  13904  lidlss  14032  lidl0cl  14039  lidlacl  14040  lidlnegcl  14041  rnglidlmsgrp  14053  2idllidld  14062  2idlridld  14063  2idlcpblrng  14079  qus1  14082  quscrng  14089  rspsn  14090  znf1o  14207  psrelbas  14228  iscnp4  14454  cnrest2r  14473  txbasval  14503  txlm  14515  xmetunirn  14594  xblss2ps  14640  blbas  14669  mopntopon  14679  isxms2  14688  metcnpi  14751  metcnpi2  14752  tgioo  14790  cncfmpt2fcntop  14835  limccl  14895  limcimolemlt  14900  limccnp2cntop  14913  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  dvrecap  14949  plyaddlem1  14983  plymullem1  14984  plycoeid3  14993  lgseisenlem4  15314