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  sn0disj  4127  opth1  4378  0nelop  4390  tfisi  4736  nnpredlt  4773  iotam  5372  ercl  6822  erth  6857  ecelqsdm  6883  phpm  7171  exmidpweq  7220  pw1if  7590  cc2lem  7638  cc3  7640  suplocexprlemmu  8091  suplocexprlemloc  8094  lincmb01cmp  10422  fzopth  10484  fzoaddel2  10625  fzosubel2  10630  fzocatel  10634  zpnn0elfzo1  10643  fzoend  10657  peano2fzor  10667  infssfzcldc  10686  infssfzledc  10687  monoord2  10944  ser3mono  10945  bcpasc  11226  zfz1isolemiso  11313  swrdclg  11444  fisum0diag2  12239  isumsplit  12283  prodmodclem3  12367  prodmodclem2a  12368  nnmindc  12836  nnminle  12837  bassetsnn  13467  basmexd  13471  basm  13472  slotm  13473  mgm1  13749  grpidd  13762  gzsumress  13771  sgrppropd  13787  ismndd  13809  mndpropd  13812  issubmnd  13814  imasmnd  13819  grpidd2  13905  imasgrp  13973  submmulg  14028  subginvcl  14045  subgcl  14046  subgsub  14048  subgmulg  14050  1nsgtrivd  14081  quseccl0g  14093  kerf1ghm  14136  prdsbasfn  14288  prdsbasprj  14289  pwsplusgval  14315  pwsmulrval  14316  pwsinvg  14322  rngass  14345  rngcl  14350  rngpropd  14361  imasrng  14362  srgcl  14381  srgass  14382  srgpcomp  14401  srgpcompp  14402  srgpcomppsc  14403  crngcom  14425  ringass  14427  ringidmlem  14434  ringidss  14441  ringpropd  14450  imasring  14478  qusring2  14480  mulgass3  14500  dvdsrd  14510  1unit  14523  unitmulcl  14529  dvrvald  14550  rdivmuldivd  14560  elrhmunit  14593  rhmunitinv  14594  lringuplu  14612  subrngmcl  14626  subrg1  14648  subrgmcl  14650  subrgdv  14655  subrgunit  14656  resrhm  14665  aprval  14700  aprirr  14704  aprsym  14705  aprcotr  14706  opprdrng  14729  lmodprop2d  14794  lidlss  14922  lidl0cl  14929  lidlacl  14930  lidlnegcl  14931  rnglidlmsgrp  14943  2idllidld  14952  2idlridld  14953  2idlcpblrng  14969  qus1  14972  quscrng  14979  rspsn  14980  znf1o  15095  assapropd  15123  psrbagfi  15168  psrbaglefifi  15172  psrelbas  15179  psrmulvalfi  15188  iscnp4  15444  cnrest2r  15463  txbasval  15493  txlm  15505  xmetunirn  15584  xblss2ps  15630  blbas  15659  mopntopon  15669  isxms2  15678  metcnpi  15741  metcnpi2  15742  tgioo  15780  cncfmpt2fcntop  15825  limccl  15885  limcimolemlt  15890  limccnp2cntop  15903  dvmulxxbr  15928  dvcoapbr  15933  dvcjbr  15934  dvrecap  15939  plyaddlem1  15973  plymullem1  15974  plycoeid3  15983  ppinprm  16260  chtnprm  16262  lgseisenlem4  16397  usgr1vr  16694  clwwlkccatlem  16846