 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 37630
 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 3413 . 2 (𝑥 = 𝐴 → (𝜑[𝐴 / 𝑥]𝜑))
21biimpac 502 1 ((𝜑𝑥 = 𝐴) → [𝐴 / 𝑥]𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  [wsbc 3402 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-sbc 3403 This theorem is referenced by:  pm13.194  37635
 Copyright terms: Public domain W3C validator