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

Theorem spsbc 3037
 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 1996 and rspsbc 3103. (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 1996 . . . 4
2 sbsbc 3029 . . . 4
31, 2sylib 188 . . 3
4 dfsbcq 3027 . . 3
53, 4syl5ib 210 . 2
65vtocleg 2888 1
 Colors of variables: wff set class Syntax hints:   wi 4  wal 1531   wceq 1633  wsb 1639   wcel 1701  wsbc 3025 This theorem is referenced by:  spsbcd  3038  sbcth  3039  sbcthdv  3040  sbceqal  3076  sbcimdv  3086  csbexg  3125  csbiebt  3151  ovmpt2dxf  6015  pm14.18  26776  sbcbi  27797  onfrALTlem3  27803  csbeq2g  27809  sbc3orgVD  28138  sbcbiVD  28163  csbingVD  28171  onfrALTlem3VD  28174  csbeq2gVD  28179  csbunigVD  28185 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1533  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-v 2824  df-sbc 3026
 Copyright terms: Public domain W3C validator