Theorem spsbcd

Description: Specialization: if a formula is true for all sets, it is true for any class which is a set. Similar to Theorem 6.11 of Quine p. 44. See also stdpc4 and rspsbc . (Contributed by Mario Carneiro, 9-Feb-2017)

	Ref	Expression
Hypotheses	spsbcd.1	|- ( ph -> A e. V )
	spsbcd.2	|- ( ph -> A. x ps )
Assertion	spsbcd	|- ( ph -> [. A / x ]. ps )

Proof

Step	Hyp	Ref	Expression
1		spsbcd.1	|- ( ph -> A e. V )
2		spsbcd.2	|- ( ph -> A. x ps )
3		spsbc	|- ( A e. V -> ( A. x ps -> [. A / x ]. ps ) )
4	1 2 3	sylc	|- ( ph -> [. A / x ]. ps )