Theorem eleqtrd 2272

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 2263	. 2 |- ( ph -> ( A e. B <-> A e. C ) )
4	1, 3	mpbid 147	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eleqtrrd  2273  3eltr3d  2276  eleqtrid  2282  eleqtrdi  2286  opth1  4266  0nelop  4278  tfisi  4620  nnpredlt  4657  iotam  5247  ercl  6600  erth  6635  ecelqsdm  6661  phpm  6923  exmidpweq  6967  cc2lem  7328  cc3  7330  suplocexprlemmu  7780  suplocexprlemloc  7783  lincmb01cmp  10072  fzopth  10130  fzoaddel2  10263  fzosubel2  10265  fzocatel  10269  zpnn0elfzo1  10278  fzoend  10292  peano2fzor  10302  monoord2  10560  ser3mono  10561  bcpasc  10840  zfz1isolemiso  10913  fisum0diag2  11593  isumsplit  11637  prodmodclem3  11721  prodmodclem2a  11722  nnmindc  12174  nnminle  12175  basmexd  12681  basm  12682  mgm1  12956  grpidd  12969  gsumress  12981  sgrppropd  12999  ismndd  13021  mndpropd  13024  issubmnd  13026  grpidd2  13116  imasgrp  13184  submmulg  13239  subginvcl  13256  subgcl  13257  subgsub  13259  subgmulg  13261  1nsgtrivd  13292  quseccl0g  13304  kerf1ghm  13347  rngass  13438  rngcl  13443  rngpropd  13454  imasrng  13455  srgcl  13469  srgass  13470  srg1zr  13486  srgpcomp  13489  srgpcompp  13490  srgpcomppsc  13491  crngcom  13513  ringass  13515  ringidmlem  13521  ringidss  13528  ringpropd  13537  imasring  13563  qusring2  13565  mulgass3  13584  dvdsrd  13593  1unit  13606  unitmulcl  13612  dvrvald  13633  rdivmuldivd  13643  elrhmunit  13676  rhmunitinv  13677  lringuplu  13695  subrngmcl  13708  subrg1  13730  subrgmcl  13732  subrgdv  13737  subrgunit  13738  resrhm  13747  aprval  13781  aprirr  13782  aprsym  13783  aprcotr  13784  lmodprop2d  13847  lidlss  13975  lidl0cl  13982  lidlacl  13983  lidlnegcl  13984  rnglidlmsgrp  13996  2idllidld  14005  2idlridld  14006  2idlcpblrng  14022  qus1  14025  quscrng  14032  rspsn  14033  znf1o  14150  psrelbas  14171  iscnp4  14397  cnrest2r  14416  txbasval  14446  txlm  14458  xmetunirn  14537  xblss2ps  14583  blbas  14612  mopntopon  14622  isxms2  14631  metcnpi  14694  metcnpi2  14695  tgioo  14733  cncfmpt2fcntop  14778  limccl  14838  limcimolemlt  14843  limccnp2cntop  14856  dvmulxxbr  14881  dvcoapbr  14886  dvcjbr  14887  dvrecap  14892  plyaddlem1  14926  plymullem1  14927  lgseisenlem4  15230