Theorem pm13.13a

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)

	Ref	Expression
Assertion	pm13.13a	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → [ 𝐴 / 𝑥 ] 𝜑 )

Proof

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