Theorem pm13.13a 44431

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

Step	Hyp	Ref	Expression
1		sbceq1a 3776	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))
2	1	biimpac 478	1 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → [𝐴 / 𝑥]𝜑)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  [wsbc 3765

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sbc 3766

This theorem is referenced by:  pm13.194  44436