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  4270  0nelop  4282  tfisi  4624  nnpredlt  4661  iotam  5251  ercl  6612  erth  6647  ecelqsdm  6673  phpm  6935  exmidpweq  6979  cc2lem  7349  cc3  7351  suplocexprlemmu  7802  suplocexprlemloc  7805  lincmb01cmp  10095  fzopth  10153  fzoaddel2  10286  fzosubel2  10288  fzocatel  10292  zpnn0elfzo1  10301  fzoend  10315  peano2fzor  10325  monoord2  10595  ser3mono  10596  bcpasc  10875  zfz1isolemiso  10948  fisum0diag2  11629  isumsplit  11673  prodmodclem3  11757  prodmodclem2a  11758  nnmindc  12226  nnminle  12227  basmexd  12763  basm  12764  prdsbasfn  12983  prdsbasprj  12984  pwsplusgval  12997  pwsmulrval  12998  mgm1  13072  grpidd  13085  gsumress  13097  sgrppropd  13115  ismndd  13139  mndpropd  13142  issubmnd  13144  imasmnd  13155  grpidd2  13243  pwsinvg  13314  imasgrp  13317  submmulg  13372  subginvcl  13389  subgcl  13390  subgsub  13392  subgmulg  13394  1nsgtrivd  13425  quseccl0g  13437  kerf1ghm  13480  rngass  13571  rngcl  13576  rngpropd  13587  imasrng  13588  srgcl  13602  srgass  13603  srg1zr  13619  srgpcomp  13622  srgpcompp  13623  srgpcomppsc  13624  crngcom  13646  ringass  13648  ringidmlem  13654  ringidss  13661  ringpropd  13670  imasring  13696  qusring2  13698  mulgass3  13717  dvdsrd  13726  1unit  13739  unitmulcl  13745  dvrvald  13766  rdivmuldivd  13776  elrhmunit  13809  rhmunitinv  13810  lringuplu  13828  subrngmcl  13841  subrg1  13863  subrgmcl  13865  subrgdv  13870  subrgunit  13871  resrhm  13880  aprval  13914  aprirr  13915  aprsym  13916  aprcotr  13917  lmodprop2d  13980  lidlss  14108  lidl0cl  14115  lidlacl  14116  lidlnegcl  14117  rnglidlmsgrp  14129  2idllidld  14138  2idlridld  14139  2idlcpblrng  14155  qus1  14158  quscrng  14165  rspsn  14166  znf1o  14283  psrelbas  14304  iscnp4  14538  cnrest2r  14557  txbasval  14587  txlm  14599  xmetunirn  14678  xblss2ps  14724  blbas  14753  mopntopon  14763  isxms2  14772  metcnpi  14835  metcnpi2  14836  tgioo  14874  cncfmpt2fcntop  14919  limccl  14979  limcimolemlt  14984  limccnp2cntop  14997  dvmulxxbr  15022  dvcoapbr  15027  dvcjbr  15028  dvrecap  15033  plyaddlem1  15067  plymullem1  15068  plycoeid3  15077  lgseisenlem4  15398