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

Theorem a4sbc 2933
 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 1896 and ra4sbc 2999. (Contributed by NM, 16-Jan-2004.)
Assertion
Ref Expression
a4sbc

Proof of Theorem a4sbc
StepHypRef Expression
1 stdpc4 1896 . . . 4
2 sbsbc 2925 . . . 4
31, 2sylib 190 . . 3
4 dfsbcq 2923 . . 3
53, 4syl5ib 212 . 2
65vtocleg 2792 1
 Colors of variables: wff set class Syntax hints:   wi 6  wal 1532   wceq 1619   wcel 1621  wsb 1882  wsbc 2921 This theorem is referenced by:  a4sbcd  2934  sbcth  2935  sbcthdv  2936  sbceqal  2972  sbcimdv  2982  csbexg  3019  csbiebt  3045  ovmpt2dxf  5825  pm14.18  26795  sbcbi  26996  onfrALTlem3  27002  csbeq2g  27008  sbc3orgVD  27317  sbcbiVD  27342  csbingVD  27350  onfrALTlem3VD  27353  csbeq2gVD  27358  csbunigVD  27364 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-12o 1664  ax-9 1684  ax-4 1692  ax-ext 2234 This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-v 2729  df-sbc 2922
 Copyright terms: Public domain W3C validator