Metamath Proof Explorer

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 φ A V
spsbcd.2 φ x ψ
Assertion spsbcd φ [˙A / x]˙ ψ


Step Hyp Ref Expression
1 spsbcd.1 φ A V
2 spsbcd.2 φ x ψ
3 spsbc A V x ψ [˙A / x]˙ ψ
4 1 2 3 sylc φ [˙A / x]˙ ψ