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

Theorem spsbc 3340
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 2094 and rspsbc 3417. (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 2094 . . . 4
2 sbsbc 3331 . . . 4
31, 2sylib 196 . . 3
4 dfsbcq 3329 . . 3
53, 4syl5ib 219 . 2
65vtocleg 3180 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393  =wceq 1395  [wsb 1739  e.wcel 1818  [.wsbc 3327
This theorem is referenced by:  spsbcd  3341  sbcth  3342  sbcthdv  3343  sbceqal  3383  sbcimdv  3396  sbcimdvOLD  3397  csbiebt  3454  csbexg  4584  csbexgOLD  4586  pm14.18  31335  sbcbi  33310  onfrALTlem3  33316  csbeq2gOLD  33322  sbc3orgVD  33651  sbcbiVD  33676  csbingVD  33684  onfrALTlem3VD  33687  csbeq2gVD  33692  csbunigVD  33698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-sbc 3328
  Copyright terms: Public domain W3C validator