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 e. V -> ( A. x ph -> [. A / x ]. ph ) )

Proof

Step	Hyp	Ref	Expression
1		stdpc4	|- ( A. x ph -> [ y / x ] ph )
2		sbsbc	|- ( [ y / x ] ph <-> [. y / x ]. ph )
3	1 2	sylib	|- ( A. x ph -> [. y / x ]. ph )
4		dfsbcq	|- ( y = A -> ( [. y / x ]. ph <-> [. A / x ]. ph ) )
5	3 4	syl5ib	|- ( y = A -> ( A. x ph -> [. A / x ]. ph ) )
6	5	vtocleg	|- ( A e. V -> ( A. x ph -> [. A / x ]. ph ) )