Theorem pm13.13a 45239

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 3753	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))
2	1	biimpac 484	1 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → [𝐴 / 𝑥]𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  [wsbc 3742

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743

This theorem is used by:  pm13.194  45244