Metamath Proof Explorer

Theorem spsbc

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. This is Frege's ninth axiom per Proposition 58 of Frege1879 p. 51. See also stdpc4 and rspsbc . (Contributed by NM, 16-Jan-2004)

Ref Expression
Assertion spsbc A V x φ [˙A / x]˙ φ


Step Hyp Ref Expression
1 stdpc4 x φ y x φ
2 sbsbc y x φ [˙y / x]˙ φ
3 1 2 sylib x φ [˙y / x]˙ φ
4 dfsbcq y = A [˙y / x]˙ φ [˙A / x]˙ φ
5 3 4 syl5ib y = A x φ [˙A / x]˙ φ
6 5 vtocleg A V x φ [˙A / x]˙ φ