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

Theorem spsbc 3165
 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. See also stdpc4 2087 and rspsbc 3231. (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 2087 . . . 4
2 sbsbc 3157 . . . 4
31, 2sylib 189 . . 3
4 dfsbcq 3155 . . 3
53, 4syl5ib 211 . 2
65vtocleg 3014 1
 Colors of variables: wff set class Syntax hints:   wi 4  wal 1549   wceq 1652  wsb 1658   wcel 1725  wsbc 3153 This theorem is referenced by:  spsbcd  3166  sbcth  3167  sbcthdv  3168  sbceqal  3204  sbcimdv  3214  csbexg  3253  csbiebt  3279  pm14.18  27596  sbcbi  28561  onfrALTlem3  28567  csbeq2g  28573  sbc3orgVD  28900  sbcbiVD  28925  csbingVD  28933  onfrALTlem3VD  28936  csbeq2gVD  28941  csbunigVD  28947 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-12 1950  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-v 2950  df-sbc 3154
 Copyright terms: Public domain W3C validator