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	|- ph
Assertion	sbcth	|- ( A e. V -> [. A / x ]. ph )

Proof

Step	Hyp	Ref	Expression
1		sbcth.1	|- ph
2	1	ax-gen	|- A. x ph
3		spsbc	|- ( A e. V -> ( A. x ph -> [. A / x ]. ph ) )
4	2 3	mpi	|- ( A e. V -> [. A / x ]. ph )