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

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

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