Theorem eleqtrd 2308

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrd.1	|- ( ph -> A e. B )
eleqtrd.2	|- ( ph -> B = C )

Assertion

Ref	Expression
eleqtrd	|- ( ph -> A e. C )

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 |- ( ph -> A e. B )
2		eleqtrd.2	. . 3 |- ( ph -> B = C )
3	2	eleq2d 2299	. 2 |- ( ph -> ( A e. B <-> A e. C ) )
4	1, 3	mpbid 147	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleqtrrd  2309  3eltr3d  2312  eleqtrid  2318  eleqtrdi  2322  opth1  4326  0nelop  4338  tfisi  4683  nnpredlt  4720  iotam  5316  ercl  6708  erth  6743  ecelqsdm  6769  phpm  7047  exmidpweq  7094  pw1if  7433  cc2lem  7475  cc3  7477  suplocexprlemmu  7928  suplocexprlemloc  7931  lincmb01cmp  10228  fzopth  10286  fzoaddel2  10425  fzosubel2  10430  fzocatel  10434  zpnn0elfzo1  10443  fzoend  10457  peano2fzor  10467  monoord2  10738  ser3mono  10739  bcpasc  11018  zfz1isolemiso  11093  swrdclg  11221  fisum0diag2  11998  isumsplit  12042  prodmodclem3  12126  prodmodclem2a  12127  nnmindc  12595  nnminle  12596  bassetsnn  13129  basmexd  13133  basm  13134  prdsbasfn  13354  prdsbasprj  13355  pwsplusgval  13368  pwsmulrval  13369  mgm1  13443  grpidd  13456  gsumress  13468  sgrppropd  13486  ismndd  13510  mndpropd  13513  issubmnd  13515  imasmnd  13526  grpidd2  13614  pwsinvg  13685  imasgrp  13688  submmulg  13743  subginvcl  13760  subgcl  13761  subgsub  13763  subgmulg  13765  1nsgtrivd  13796  quseccl0g  13808  kerf1ghm  13851  rngass  13942  rngcl  13947  rngpropd  13958  imasrng  13959  srgcl  13973  srgass  13974  srg1zr  13990  srgpcomp  13993  srgpcompp  13994  srgpcomppsc  13995  crngcom  14017  ringass  14019  ringidmlem  14025  ringidss  14032  ringpropd  14041  imasring  14067  qusring2  14069  mulgass3  14088  dvdsrd  14098  1unit  14111  unitmulcl  14117  dvrvald  14138  rdivmuldivd  14148  elrhmunit  14181  rhmunitinv  14182  lringuplu  14200  subrngmcl  14213  subrg1  14235  subrgmcl  14237  subrgdv  14242  subrgunit  14243  resrhm  14252  aprval  14286  aprirr  14287  aprsym  14288  aprcotr  14289  lmodprop2d  14352  lidlss  14480  lidl0cl  14487  lidlacl  14488  lidlnegcl  14489  rnglidlmsgrp  14501  2idllidld  14510  2idlridld  14511  2idlcpblrng  14527  qus1  14530  quscrng  14537  rspsn  14538  znf1o  14655  psrbagfi  14677  psrelbas  14679  iscnp4  14932  cnrest2r  14951  txbasval  14981  txlm  14993  xmetunirn  15072  xblss2ps  15118  blbas  15147  mopntopon  15157  isxms2  15166  metcnpi  15229  metcnpi2  15230  tgioo  15268  cncfmpt2fcntop  15313  limccl  15373  limcimolemlt  15378  limccnp2cntop  15391  dvmulxxbr  15416  dvcoapbr  15421  dvcjbr  15422  dvrecap  15427  plyaddlem1  15461  plymullem1  15462  plycoeid3  15471  lgseisenlem4  15792  usgr1vr  16087  clwwlkccatlem  16195