Theorem eleqtrd 2313

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

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

This theorem is referenced by:  eleqtrrd  2314  3eltr3d  2317  eleqtrid  2323  eleqtrdi  2327  opth1  4357  0nelop  4369  tfisi  4714  nnpredlt  4751  iotam  5349  ercl  6791  erth  6826  ecelqsdm  6852  phpm  7133  exmidpweq  7182  pw1if  7548  cc2lem  7596  cc3  7598  suplocexprlemmu  8049  suplocexprlemloc  8052  lincmb01cmp  10358  fzopth  10419  fzoaddel2  10560  fzosubel2  10565  fzocatel  10569  zpnn0elfzo1  10578  fzoend  10592  peano2fzor  10602  infssfzcldc  10621  infssfzledc  10622  monoord2  10875  ser3mono  10876  bcpasc  11156  zfz1isolemiso  11239  swrdclg  11370  fisum0diag2  12162  isumsplit  12206  prodmodclem3  12290  prodmodclem2a  12291  nnmindc  12759  nnminle  12760  bassetsnn  13357  basmexd  13361  basm  13362  mgm1  13637  grpidd  13650  gsumress  13662  sgrppropd  13680  ismndd  13702  mndpropd  13705  issubmnd  13707  imasmnd  13712  grpidd2  13800  imasgrp  13868  submmulg  13923  subginvcl  13940  subgcl  13941  subgsub  13943  subgmulg  13945  1nsgtrivd  13976  quseccl0g  13988  kerf1ghm  14031  prdsbasfn  14127  prdsbasprj  14128  pwsplusgval  14154  pwsmulrval  14155  pwsinvg  14161  rngass  14182  rngcl  14187  rngpropd  14198  imasrng  14199  srgcl  14217  srgass  14218  srgpcomp  14237  srgpcompp  14238  srgpcomppsc  14239  crngcom  14261  ringass  14263  ringidmlem  14269  ringidss  14276  ringpropd  14285  imasring  14311  qusring2  14313  mulgass3  14333  dvdsrd  14343  1unit  14356  unitmulcl  14362  dvrvald  14383  rdivmuldivd  14393  elrhmunit  14426  rhmunitinv  14427  lringuplu  14445  subrngmcl  14459  subrg1  14481  subrgmcl  14483  subrgdv  14488  subrgunit  14489  resrhm  14498  aprval  14533  aprirr  14537  aprsym  14538  aprcotr  14539  opprdrng  14562  lmodprop2d  14626  lidlss  14754  lidl0cl  14761  lidlacl  14762  lidlnegcl  14763  rnglidlmsgrp  14775  2idllidld  14784  2idlridld  14785  2idlcpblrng  14801  qus1  14804  quscrng  14811  rspsn  14812  znf1o  14929  psrbagfi  14953  psrelbas  14960  iscnp4  15213  cnrest2r  15232  txbasval  15262  txlm  15274  xmetunirn  15353  xblss2ps  15399  blbas  15428  mopntopon  15438  isxms2  15447  metcnpi  15510  metcnpi2  15511  tgioo  15549  cncfmpt2fcntop  15594  limccl  15654  limcimolemlt  15659  limccnp2cntop  15672  dvmulxxbr  15697  dvcoapbr  15702  dvcjbr  15703  dvrecap  15708  plyaddlem1  15742  plymullem1  15743  plycoeid3  15752  lgseisenlem4  16076  usgr1vr  16373  clwwlkccatlem  16525