Theorem eleqtrd 2272

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

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

This theorem is referenced by:  eleqtrrd  2273  3eltr3d  2276  eleqtrid  2282  eleqtrdi  2286  opth1  4265  0nelop  4277  tfisi  4619  nnpredlt  4656  iotam  5246  ercl  6598  erth  6633  ecelqsdm  6659  phpm  6921  exmidpweq  6965  cc2lem  7326  cc3  7328  suplocexprlemmu  7778  suplocexprlemloc  7781  lincmb01cmp  10069  fzopth  10127  fzoaddel2  10260  fzosubel2  10262  fzocatel  10266  zpnn0elfzo1  10275  fzoend  10289  peano2fzor  10299  monoord2  10557  ser3mono  10558  bcpasc  10837  zfz1isolemiso  10910  fisum0diag2  11590  isumsplit  11634  prodmodclem3  11718  prodmodclem2a  11719  nnmindc  12171  nnminle  12172  basmexd  12678  basm  12679  mgm1  12953  grpidd  12966  gsumress  12978  sgrppropd  12996  ismndd  13018  mndpropd  13021  issubmnd  13023  grpidd2  13113  imasgrp  13181  submmulg  13236  subginvcl  13253  subgcl  13254  subgsub  13256  subgmulg  13258  1nsgtrivd  13289  quseccl0g  13301  kerf1ghm  13344  rngass  13435  rngcl  13440  rngpropd  13451  imasrng  13452  srgcl  13466  srgass  13467  srg1zr  13483  srgpcomp  13486  srgpcompp  13487  srgpcomppsc  13488  crngcom  13510  ringass  13512  ringidmlem  13518  ringidss  13525  ringpropd  13534  imasring  13560  qusring2  13562  mulgass3  13581  dvdsrd  13590  1unit  13603  unitmulcl  13609  dvrvald  13630  rdivmuldivd  13640  elrhmunit  13673  rhmunitinv  13674  lringuplu  13692  subrngmcl  13705  subrg1  13727  subrgmcl  13729  subrgdv  13734  subrgunit  13735  resrhm  13744  aprval  13778  aprirr  13779  aprsym  13780  aprcotr  13781  lmodprop2d  13844  lidlss  13972  lidl0cl  13979  lidlacl  13980  lidlnegcl  13981  rnglidlmsgrp  13993  2idllidld  14002  2idlridld  14003  2idlcpblrng  14019  qus1  14022  quscrng  14029  rspsn  14030  znf1o  14139  psrelbas  14160  iscnp4  14386  cnrest2r  14405  txbasval  14435  txlm  14447  xmetunirn  14526  xblss2ps  14572  blbas  14601  mopntopon  14611  isxms2  14620  metcnpi  14683  metcnpi2  14684  tgioo  14714  cncfmpt2fcntop  14753  limccl  14813  limcimolemlt  14818  limccnp2cntop  14831  dvmulxxbr  14851  dvcoapbr  14856  dvcjbr  14857  dvrecap  14862  plyaddlem1  14893  plymullem1  14894  lgseisenlem4  15189