Theorem eleqtrd 2284

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleqtrrd  2285  3eltr3d  2288  eleqtrid  2294  eleqtrdi  2298  opth1  4281  0nelop  4293  tfisi  4636  nnpredlt  4673  iotam  5264  ercl  6633  erth  6668  ecelqsdm  6694  phpm  6964  exmidpweq  7008  cc2lem  7380  cc3  7382  suplocexprlemmu  7833  suplocexprlemloc  7836  lincmb01cmp  10127  fzopth  10185  fzoaddel2  10321  fzosubel2  10326  fzocatel  10330  zpnn0elfzo1  10339  fzoend  10353  peano2fzor  10363  monoord2  10633  ser3mono  10634  bcpasc  10913  zfz1isolemiso  10986  swrdclg  11106  fisum0diag2  11791  isumsplit  11835  prodmodclem3  11919  prodmodclem2a  11920  nnmindc  12388  nnminle  12389  basmexd  12925  basm  12926  prdsbasfn  13146  prdsbasprj  13147  pwsplusgval  13160  pwsmulrval  13161  mgm1  13235  grpidd  13248  gsumress  13260  sgrppropd  13278  ismndd  13302  mndpropd  13305  issubmnd  13307  imasmnd  13318  grpidd2  13406  pwsinvg  13477  imasgrp  13480  submmulg  13535  subginvcl  13552  subgcl  13553  subgsub  13555  subgmulg  13557  1nsgtrivd  13588  quseccl0g  13600  kerf1ghm  13643  rngass  13734  rngcl  13739  rngpropd  13750  imasrng  13751  srgcl  13765  srgass  13766  srg1zr  13782  srgpcomp  13785  srgpcompp  13786  srgpcomppsc  13787  crngcom  13809  ringass  13811  ringidmlem  13817  ringidss  13824  ringpropd  13833  imasring  13859  qusring2  13861  mulgass3  13880  dvdsrd  13889  1unit  13902  unitmulcl  13908  dvrvald  13929  rdivmuldivd  13939  elrhmunit  13972  rhmunitinv  13973  lringuplu  13991  subrngmcl  14004  subrg1  14026  subrgmcl  14028  subrgdv  14033  subrgunit  14034  resrhm  14043  aprval  14077  aprirr  14078  aprsym  14079  aprcotr  14080  lmodprop2d  14143  lidlss  14271  lidl0cl  14278  lidlacl  14279  lidlnegcl  14280  rnglidlmsgrp  14292  2idllidld  14301  2idlridld  14302  2idlcpblrng  14318  qus1  14321  quscrng  14328  rspsn  14329  znf1o  14446  psrbagfi  14468  psrelbas  14470  iscnp4  14723  cnrest2r  14742  txbasval  14772  txlm  14784  xmetunirn  14863  xblss2ps  14909  blbas  14938  mopntopon  14948  isxms2  14957  metcnpi  15020  metcnpi2  15021  tgioo  15059  cncfmpt2fcntop  15104  limccl  15164  limcimolemlt  15169  limccnp2cntop  15182  dvmulxxbr  15207  dvcoapbr  15212  dvcjbr  15213  dvrecap  15218  plyaddlem1  15252  plymullem1  15253  plycoeid3  15262  lgseisenlem4  15583