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	$$⊢\phi \to A\in V$$
	spsbcd.2	$$⊢\phi \to \forall x\psi$$
Assertion	spsbcd	$$⊢\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$

Proof

Step	Hyp	Ref	Expression
1		spsbcd.1	$$⊢\phi \to A\in V$$
2		spsbcd.2	$$⊢\phi \to \forall x\psi$$
3		spsbc	$$⊢A\in V\to \left(\forall x\psi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
4	1 2 3	sylc	$$⊢\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$