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 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleqtrrd  2318  3eltr3d  2321  eleqtrid  2327  eleqtrdi  2331  opth1  4376  0nelop  4388  tfisi  4734  nnpredlt  4771  iotam  5369  ercl  6818  erth  6853  ecelqsdm  6879  phpm  7167  exmidpweq  7216  pw1if  7585  cc2lem  7633  cc3  7635  suplocexprlemmu  8086  suplocexprlemloc  8089  lincmb01cmp  10416  fzopth  10478  fzoaddel2  10619  fzosubel2  10624  fzocatel  10628  zpnn0elfzo1  10637  fzoend  10651  peano2fzor  10661  infssfzcldc  10680  infssfzledc  10681  monoord2  10938  ser3mono  10939  bcpasc  11220  zfz1isolemiso  11307  swrdclg  11438  fisum0diag2  12233  isumsplit  12277  prodmodclem3  12361  prodmodclem2a  12362  nnmindc  12830  nnminle  12831  bassetsnn  13461  basmexd  13465  basm  13466  slotm  13467  mgm1  13743  grpidd  13756  gzsumress  13765  sgrppropd  13781  ismndd  13803  mndpropd  13806  issubmnd  13808  imasmnd  13813  grpidd2  13899  imasgrp  13967  submmulg  14022  subginvcl  14039  subgcl  14040  subgsub  14042  subgmulg  14044  1nsgtrivd  14075  quseccl0g  14087  kerf1ghm  14130  prdsbasfn  14265  prdsbasprj  14266  pwsplusgval  14292  pwsmulrval  14293  pwsinvg  14299  rngass  14322  rngcl  14327  rngpropd  14338  imasrng  14339  srgcl  14358  srgass  14359  srgpcomp  14378  srgpcompp  14379  srgpcomppsc  14380  crngcom  14402  ringass  14404  ringidmlem  14411  ringidss  14418  ringpropd  14427  imasring  14453  qusring2  14455  mulgass3  14475  dvdsrd  14485  1unit  14498  unitmulcl  14504  dvrvald  14525  rdivmuldivd  14535  elrhmunit  14568  rhmunitinv  14569  lringuplu  14587  subrngmcl  14601  subrg1  14623  subrgmcl  14625  subrgdv  14630  subrgunit  14631  resrhm  14640  aprval  14675  aprirr  14679  aprsym  14680  aprcotr  14681  opprdrng  14704  lmodprop2d  14769  lidlss  14897  lidl0cl  14904  lidlacl  14905  lidlnegcl  14906  rnglidlmsgrp  14918  2idllidld  14927  2idlridld  14928  2idlcpblrng  14944  qus1  14947  quscrng  14954  rspsn  14955  znf1o  15070  assapropd  15098  psrbagfi  15143  psrbaglefifi  15147  psrelbas  15151  psrmulvalfi  15160  iscnp4  15410  cnrest2r  15429  txbasval  15459  txlm  15471  xmetunirn  15550  xblss2ps  15596  blbas  15625  mopntopon  15635  isxms2  15644  metcnpi  15707  metcnpi2  15708  tgioo  15746  cncfmpt2fcntop  15791  limccl  15851  limcimolemlt  15856  limccnp2cntop  15869  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  dvrecap  15905  plyaddlem1  15939  plymullem1  15940  plycoeid3  15949  ppinprm  16221  chtnprm  16223  lgseisenlem4  16358  usgr1vr  16655  clwwlkccatlem  16807