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

Theorem spsbc 3707
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 2074 and rspsbc 3791. (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 2074 . . . 4 (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑)
2 sbsbc 3698 . . . 4 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
31, 2sylib 221 . . 3 (∀𝑥𝜑[𝑦 / 𝑥]𝜑)
4 dfsbcq 3696 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
53, 4syl5ib 247 . 2 (𝑦 = 𝐴 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))
65vtocleg 3497 1 (𝐴𝑉 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1541   = wceq 1543  [wsb 2070  wcel 2110  [wsbc 3694
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 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3695
This theorem is referenced by:  spsbcd  3708  sbcth  3709  sbcthdv  3710  sbceqalOLD  3762  sbcimdvOLD  3770  csbiebt  3841  csbexg  5203  pm14.18  41719  sbcbi  41832  onfrALTlem3  41837  sbc3orgVD  42144  sbcbiVD  42169  csbingVD  42177  onfrALTlem3VD  42180  csbeq2gVD  42185  csbunigVD  42191
  Copyright terms: Public domain W3C validator