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  7351  cc3  7353  suplocexprlemmu  7804  suplocexprlemloc  7807  lincmb01cmp  10097  fzopth  10155  fzoaddel2  10288  fzosubel2  10290  fzocatel  10294  zpnn0elfzo1  10303  fzoend  10317  peano2fzor  10327  monoord2  10597  ser3mono  10598  bcpasc  10877  zfz1isolemiso  10950  fisum0diag2  11631  isumsplit  11675  prodmodclem3  11759  prodmodclem2a  11760  nnmindc  12228  nnminle  12229  basmexd  12765  basm  12766  prdsbasfn  12985  prdsbasprj  12986  pwsplusgval  12999  pwsmulrval  13000  mgm1  13074  grpidd  13087  gsumress  13099  sgrppropd  13117  ismndd  13141  mndpropd  13144  issubmnd  13146  imasmnd  13157  grpidd2  13245  pwsinvg  13316  imasgrp  13319  submmulg  13374  subginvcl  13391  subgcl  13392  subgsub  13394  subgmulg  13396  1nsgtrivd  13427  quseccl0g  13439  kerf1ghm  13482  rngass  13573  rngcl  13578  rngpropd  13589  imasrng  13590  srgcl  13604  srgass  13605  srg1zr  13621  srgpcomp  13624  srgpcompp  13625  srgpcomppsc  13626  crngcom  13648  ringass  13650  ringidmlem  13656  ringidss  13663  ringpropd  13672  imasring  13698  qusring2  13700  mulgass3  13719  dvdsrd  13728  1unit  13741  unitmulcl  13747  dvrvald  13768  rdivmuldivd  13778  elrhmunit  13811  rhmunitinv  13812  lringuplu  13830  subrngmcl  13843  subrg1  13865  subrgmcl  13867  subrgdv  13872  subrgunit  13873  resrhm  13882  aprval  13916  aprirr  13917  aprsym  13918  aprcotr  13919  lmodprop2d  13982  lidlss  14110  lidl0cl  14117  lidlacl  14118  lidlnegcl  14119  rnglidlmsgrp  14131  2idllidld  14140  2idlridld  14141  2idlcpblrng  14157  qus1  14160  quscrng  14167  rspsn  14168  znf1o  14285  psrbagfi  14307  psrelbas  14309  iscnp4  14562  cnrest2r  14581  txbasval  14611  txlm  14623  xmetunirn  14702  xblss2ps  14748  blbas  14777  mopntopon  14787  isxms2  14796  metcnpi  14859  metcnpi2  14860  tgioo  14898  cncfmpt2fcntop  14943  limccl  15003  limcimolemlt  15008  limccnp2cntop  15021  dvmulxxbr  15046  dvcoapbr  15051  dvcjbr  15052  dvrecap  15057  plyaddlem1  15091  plymullem1  15092  plycoeid3  15101  lgseisenlem4  15422