MPE Home 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  |-  ( A  e.  V  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)

Proof of Theorem a4sbc
StepHypRef Expression
1 stdpc4 1896 . . . 4  |-  ( A. x ph  ->  [ y  /  x ] ph )
2 sbsbc 2925 . . . 4  |-  ( [ y  /  x ] ph 
<-> 
[. y  /  x ]. ph )
31, 2sylib 190 . . 3  |-  ( A. x ph  ->  [. y  /  x ]. ph )
4 dfsbcq 2923 . . 3  |-  ( y  =  A  ->  ( [. y  /  x ]. ph  <->  [. A  /  x ]. ph ) )
53, 4syl5ib 212 . 2  |-  ( y  =  A  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
65vtocleg 2792 1  |-  ( A  e.  V  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532    = wceq 1619    e. 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