Theorem eleqtrd 2317

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  eleqtrrd  2318  3eltr3d  2321  eleqtrid  2327  eleqtrdi  2331  opth1  4371  0nelop  4383  tfisi  4729  nnpredlt  4766  iotam  5364  ercl  6808  erth  6843  ecelqsdm  6869  phpm  7157  exmidpweq  7206  pw1if  7574  cc2lem  7622  cc3  7624  suplocexprlemmu  8075  suplocexprlemloc  8078  lincmb01cmp  10384  fzopth  10445  fzoaddel2  10586  fzosubel2  10591  fzocatel  10595  zpnn0elfzo1  10604  fzoend  10618  peano2fzor  10628  infssfzcldc  10647  infssfzledc  10648  monoord2  10901  ser3mono  10902  bcpasc  11182  zfz1isolemiso  11269  swrdclg  11400  fisum0diag2  12192  isumsplit  12236  prodmodclem3  12320  prodmodclem2a  12321  nnmindc  12789  nnminle  12790  bassetsnn  13387  basmexd  13391  basm  13392  mgm1  13667  grpidd  13680  gzsumress  13689  sgrppropd  13705  ismndd  13727  mndpropd  13730  issubmnd  13732  imasmnd  13737  grpidd2  13823  imasgrp  13891  submmulg  13946  subginvcl  13963  subgcl  13964  subgsub  13966  subgmulg  13968  1nsgtrivd  13999  quseccl0g  14011  kerf1ghm  14054  prdsbasfn  14158  prdsbasprj  14159  pwsplusgval  14185  pwsmulrval  14186  pwsinvg  14192  rngass  14213  rngcl  14218  rngpropd  14229  imasrng  14230  srgcl  14248  srgass  14249  srgpcomp  14268  srgpcompp  14269  srgpcomppsc  14270  crngcom  14292  ringass  14294  ringidmlem  14300  ringidss  14307  ringpropd  14316  imasring  14342  qusring2  14344  mulgass3  14364  dvdsrd  14374  1unit  14387  unitmulcl  14393  dvrvald  14414  rdivmuldivd  14424  elrhmunit  14457  rhmunitinv  14458  lringuplu  14476  subrngmcl  14490  subrg1  14512  subrgmcl  14514  subrgdv  14519  subrgunit  14520  resrhm  14529  aprval  14564  aprirr  14568  aprsym  14569  aprcotr  14570  opprdrng  14593  lmodprop2d  14657  lidlss  14785  lidl0cl  14792  lidlacl  14793  lidlnegcl  14794  rnglidlmsgrp  14806  2idllidld  14815  2idlridld  14816  2idlcpblrng  14832  qus1  14835  quscrng  14842  rspsn  14843  znf1o  14958  psrbagfi  14982  psrelbas  14989  iscnp4  15242  cnrest2r  15261  txbasval  15291  txlm  15303  xmetunirn  15382  xblss2ps  15428  blbas  15457  mopntopon  15467  isxms2  15476  metcnpi  15539  metcnpi2  15540  tgioo  15578  cncfmpt2fcntop  15623  limccl  15683  limcimolemlt  15688  limccnp2cntop  15701  dvmulxxbr  15726  dvcoapbr  15731  dvcjbr  15732  dvrecap  15737  plyaddlem1  15771  plymullem1  15772  plycoeid3  15781  lgseisenlem4  16106  usgr1vr  16403  clwwlkccatlem  16555