This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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]˙ ψ

Proof

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]˙ ψ