Theorem eleqtrd 2286

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  eleqtrrd  2287  3eltr3d  2290  eleqtrid  2296  eleqtrdi  2300  opth1  4298  0nelop  4310  tfisi  4653  nnpredlt  4690  iotam  5282  ercl  6654  erth  6689  ecelqsdm  6715  phpm  6988  exmidpweq  7032  pw1if  7371  cc2lem  7413  cc3  7415  suplocexprlemmu  7866  suplocexprlemloc  7869  lincmb01cmp  10160  fzopth  10218  fzoaddel2  10356  fzosubel2  10361  fzocatel  10365  zpnn0elfzo1  10374  fzoend  10388  peano2fzor  10398  monoord2  10668  ser3mono  10669  bcpasc  10948  zfz1isolemiso  11021  swrdclg  11141  fisum0diag2  11873  isumsplit  11917  prodmodclem3  12001  prodmodclem2a  12002  nnmindc  12470  nnminle  12471  basmexd  13007  basm  13008  prdsbasfn  13228  prdsbasprj  13229  pwsplusgval  13242  pwsmulrval  13243  mgm1  13317  grpidd  13330  gsumress  13342  sgrppropd  13360  ismndd  13384  mndpropd  13387  issubmnd  13389  imasmnd  13400  grpidd2  13488  pwsinvg  13559  imasgrp  13562  submmulg  13617  subginvcl  13634  subgcl  13635  subgsub  13637  subgmulg  13639  1nsgtrivd  13670  quseccl0g  13682  kerf1ghm  13725  rngass  13816  rngcl  13821  rngpropd  13832  imasrng  13833  srgcl  13847  srgass  13848  srg1zr  13864  srgpcomp  13867  srgpcompp  13868  srgpcomppsc  13869  crngcom  13891  ringass  13893  ringidmlem  13899  ringidss  13906  ringpropd  13915  imasring  13941  qusring2  13943  mulgass3  13962  dvdsrd  13971  1unit  13984  unitmulcl  13990  dvrvald  14011  rdivmuldivd  14021  elrhmunit  14054  rhmunitinv  14055  lringuplu  14073  subrngmcl  14086  subrg1  14108  subrgmcl  14110  subrgdv  14115  subrgunit  14116  resrhm  14125  aprval  14159  aprirr  14160  aprsym  14161  aprcotr  14162  lmodprop2d  14225  lidlss  14353  lidl0cl  14360  lidlacl  14361  lidlnegcl  14362  rnglidlmsgrp  14374  2idllidld  14383  2idlridld  14384  2idlcpblrng  14400  qus1  14403  quscrng  14410  rspsn  14411  znf1o  14528  psrbagfi  14550  psrelbas  14552  iscnp4  14805  cnrest2r  14824  txbasval  14854  txlm  14866  xmetunirn  14945  xblss2ps  14991  blbas  15020  mopntopon  15030  isxms2  15039  metcnpi  15102  metcnpi2  15103  tgioo  15141  cncfmpt2fcntop  15186  limccl  15246  limcimolemlt  15251  limccnp2cntop  15264  dvmulxxbr  15289  dvcoapbr  15294  dvcjbr  15295  dvrecap  15300  plyaddlem1  15334  plymullem1  15335  plycoeid3  15344  lgseisenlem4  15665