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

Theorem spsbc 3791
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 2072 and rspsbc 3874. (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 2072 . . . 4 (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑)
2 sbsbc 3782 . . . 4 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
31, 2sylib 217 . . 3 (∀𝑥𝜑[𝑦 / 𝑥]𝜑)
4 dfsbcq 3780 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
53, 4imbitrid 243 . 2 (𝑦 = 𝐴 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))
65vtocleg 3546 1 (𝐴𝑉 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540   = wceq 1542  [wsb 2068  wcel 2107  [wsbc 3778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779
This theorem is referenced by:  spsbcd  3792  sbcth  3793  sbcthdv  3794  sbceqalOLD  3845  sbcimdvOLD  3853  csbiebt  3924  csbexg  5311  pm14.18  43187  sbcbi  43300  onfrALTlem3  43305  sbc3orgVD  43612  sbcbiVD  43637  csbingVD  43645  onfrALTlem3VD  43648  csbeq2gVD  43653  csbunigVD  43659
  Copyright terms: Public domain W3C validator