Theorem eleqtrd 2310

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleqtrrd  2311  3eltr3d  2314  eleqtrid  2320  eleqtrdi  2324  opth1  4328  0nelop  4340  tfisi  4685  nnpredlt  4722  iotam  5318  ercl  6712  erth  6747  ecelqsdm  6773  phpm  7051  exmidpweq  7100  pw1if  7442  cc2lem  7484  cc3  7486  suplocexprlemmu  7937  suplocexprlemloc  7940  lincmb01cmp  10237  fzopth  10295  fzoaddel2  10434  fzosubel2  10439  fzocatel  10443  zpnn0elfzo1  10452  fzoend  10466  peano2fzor  10476  monoord2  10747  ser3mono  10748  bcpasc  11027  zfz1isolemiso  11102  swrdclg  11230  fisum0diag2  12007  isumsplit  12051  prodmodclem3  12135  prodmodclem2a  12136  nnmindc  12604  nnminle  12605  bassetsnn  13138  basmexd  13142  basm  13143  prdsbasfn  13363  prdsbasprj  13364  pwsplusgval  13377  pwsmulrval  13378  mgm1  13452  grpidd  13465  gsumress  13477  sgrppropd  13495  ismndd  13519  mndpropd  13522  issubmnd  13524  imasmnd  13535  grpidd2  13623  pwsinvg  13694  imasgrp  13697  submmulg  13752  subginvcl  13769  subgcl  13770  subgsub  13772  subgmulg  13774  1nsgtrivd  13805  quseccl0g  13817  kerf1ghm  13860  rngass  13951  rngcl  13956  rngpropd  13967  imasrng  13968  srgcl  13982  srgass  13983  srg1zr  13999  srgpcomp  14002  srgpcompp  14003  srgpcomppsc  14004  crngcom  14026  ringass  14028  ringidmlem  14034  ringidss  14041  ringpropd  14050  imasring  14076  qusring2  14078  mulgass3  14097  dvdsrd  14107  1unit  14120  unitmulcl  14126  dvrvald  14147  rdivmuldivd  14157  elrhmunit  14190  rhmunitinv  14191  lringuplu  14209  subrngmcl  14222  subrg1  14244  subrgmcl  14246  subrgdv  14251  subrgunit  14252  resrhm  14261  aprval  14295  aprirr  14296  aprsym  14297  aprcotr  14298  lmodprop2d  14361  lidlss  14489  lidl0cl  14496  lidlacl  14497  lidlnegcl  14498  rnglidlmsgrp  14510  2idllidld  14519  2idlridld  14520  2idlcpblrng  14536  qus1  14539  quscrng  14546  rspsn  14547  znf1o  14664  psrbagfi  14686  psrelbas  14688  iscnp4  14941  cnrest2r  14960  txbasval  14990  txlm  15002  xmetunirn  15081  xblss2ps  15127  blbas  15156  mopntopon  15166  isxms2  15175  metcnpi  15238  metcnpi2  15239  tgioo  15277  cncfmpt2fcntop  15322  limccl  15382  limcimolemlt  15387  limccnp2cntop  15400  dvmulxxbr  15425  dvcoapbr  15430  dvcjbr  15431  dvrecap  15436  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  lgseisenlem4  15801  usgr1vr  16098  clwwlkccatlem  16250