Users' Mathboxes Mathbox for Andrew Salmon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pm13.13a Unicode version

Theorem pm13.13a 27113
Description: One result of theorem *13.13 in [WhiteheadRussell] p. 178. A note on the section - to make the theorems more usable, and because inequality is notation for set theory (it is not defined in the predicate calculus section), this section will use classes instead of sets. (Contributed by Andrew Salmon, 3-Jun-2011.)
Assertion
Ref Expression
pm13.13a  |-  ( (
ph  /\  x  =  A )  ->  [. A  /  x ]. ph )

Proof of Theorem pm13.13a
StepHypRef Expression
1 sbceq1a 3087 . 2  |-  ( x  =  A  ->  ( ph 
<-> 
[. A  /  x ]. ph ) )
21biimpac 472 1  |-  ( (
ph  /\  x  =  A )  ->  [. A  /  x ]. ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1647   [.wsbc 3077
This theorem is referenced by:  pm13.194  27118
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-sbc 3078
  Copyright terms: Public domain W3C validator