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

Theorem pm13.13a 27277
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 3115 . 2  |-  ( x  =  A  ->  ( ph 
<-> 
[. A  /  x ]. ph ) )
21biimpac 473 1  |-  ( (
ph  /\  x  =  A )  ->  [. A  /  x ]. ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649   [.wsbc 3105
This theorem is referenced by:  pm13.194  27282
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-sbc 3106
  Copyright terms: Public domain W3C validator