ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eleqtrd Unicode version

Theorem eleqtrd 2132
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
StepHypRef Expression
1 eleqtrd.1 . 2  |-  ( ph  ->  A  e.  B )
2 eleqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32eleq2d 2123 . 2  |-  ( ph  ->  ( A  e.  B  <->  A  e.  C ) )
41, 3mpbid 139 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259    e. wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  eleqtrrd  2133  3eltr3d  2136  syl5eleq  2142  syl6eleq  2146  opth1  4001  0nelop  4013  tfisi  4338  ercl  6148  erth  6181  ecelqsdm  6207  phpm  6358  lincmb01cmp  8972  fzopth  9026  fzoaddel2  9151  fzosubel2  9153  fzocatel  9157  zpnn0elfzo1  9166  fzoend  9180  peano2fzor  9190  monoord2  9400  isermono  9401  bcpasc  9634
  Copyright terms: Public domain W3C validator