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

Theorem pm13.13a 44426
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 ((𝜑𝑥 = 𝐴) → [𝐴 / 𝑥]𝜑)

Proof of Theorem pm13.13a
StepHypRef Expression
1 sbceq1a 3799 . 2 (𝑥 = 𝐴 → (𝜑[𝐴 / 𝑥]𝜑))
21biimpac 478 1 ((𝜑𝑥 = 𝐴) → [𝐴 / 𝑥]𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  [wsbc 3788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789
This theorem is referenced by:  pm13.194  44431
  Copyright terms: Public domain W3C validator