Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  spsbc Structured version   Visualization version   GIF version

Theorem spsbc 3735
 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 2073 and rspsbc 3810. (Contributed by NM, 16-Jan-2004.)
Assertion
Ref Expression
spsbc (𝐴𝑉 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))

Proof of Theorem spsbc
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 stdpc4 2073 . . . 4 (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑)
2 sbsbc 3726 . . . 4 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
31, 2sylib 221 . . 3 (∀𝑥𝜑[𝑦 / 𝑥]𝜑)
4 dfsbcq 3724 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
53, 4syl5ib 247 . 2 (𝑦 = 𝐴 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))
65vtocleg 3530 1 (𝐴𝑉 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1536   = wceq 1538  [wsb 2069   ∈ wcel 2111  [wsbc 3722 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sbc 3723 This theorem is referenced by:  spsbcd  3736  sbcth  3737  sbcthdv  3738  sbceqal  3784  sbcimdv  3791  csbiebt  3859  csbexg  5182  pm14.18  41303  sbcbi  41416  onfrALTlem3  41421  sbc3orgVD  41728  sbcbiVD  41753  csbingVD  41761  onfrALTlem3VD  41764  csbeq2gVD  41769  csbunigVD  41775
 Copyright terms: Public domain W3C validator