Theorem sbcth

Description: A substitution into a theorem remains true (when A is a set). (Contributed by NM, 5-Nov-2005)

	Ref	Expression
Hypothesis	sbcth.1	⊢ 𝜑
Assertion	sbcth	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbcth.1	⊢ 𝜑
2	1	ax-gen	⊢ ∀ 𝑥 𝜑
3		spsbc	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 𝜑 → [ 𝐴 / 𝑥 ] 𝜑 ) )
4	2 3	mpi	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 / 𝑥 ] 𝜑 )