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	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 𝜑 → [ 𝐴 / 𝑥 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		stdpc4	⊢ ( ∀ 𝑥 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 )
2		sbsbc	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 )
3	1 2	sylib	⊢ ( ∀ 𝑥 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 )
4		dfsbcq	⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
5	3 4	imbitrid	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 𝜑 → [ 𝐴 / 𝑥 ] 𝜑 ) )
6	5	vtocleg	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 𝜑 → [ 𝐴 / 𝑥 ] 𝜑 ) )