Theorem spsbc 3738

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 2080 and rspsbc 3813. (Contributed by NM, 16-Jan-2004.)

Assertion

Ref	Expression
spsbc	⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑))

Proof of Theorem spsbc

Dummy variable 𝑦 is distinct from all other variables.

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

Syntax hints:   → wi 4  ∀wal 1546   = wceq 1548  [wsb 2074   ∈ wcel 2121  [wsbc 3725

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-sbc 3726

This theorem is referenced by:  spsbcd  3739  sbcth  3740  sbcthdv  3741  csbiebt  3862  csbexg  5235  pm14.18  44887  sbcbi  44998  onfrALTlem3  45003  sbc3orgVD  45309  sbcbiVD  45334  csbingVD  45342  onfrALTlem3VD  45345  csbeq2gVD  45350  csbunigVD  45356