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

Theorem a4sbc 2947
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 1897 and ra4sbc 3013. (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 1897 . . . 4  |-  ( A. x ph  ->  [ y  /  x ] ph )
2 sbsbc 2939 . . . 4  |-  ( [ y  /  x ] ph 
<-> 
[. y  /  x ]. ph )
31, 2sylib 190 . . 3  |-  ( A. x ph  ->  [. y  /  x ]. ph )
4 dfsbcq 2937 . . 3  |-  ( y  =  A  ->  ( [. y  /  x ]. ph  <->  [. A  /  x ]. ph ) )
53, 4syl5ib 212 . 2  |-  ( y  =  A  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
65vtocleg 2805 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 1883   [.wsbc 2935
This theorem is referenced by:  a4sbcd  2948  sbcth  2949  sbcthdv  2950  sbceqal  2986  sbcimdv  2996  csbexg  3033  csbiebt  3059  ovmpt2dxf  5872  pm14.18  26961  sbcbi  27319  onfrALTlem3  27325  csbeq2g  27331  sbc3orgVD  27640  sbcbiVD  27665  csbingVD  27673  onfrALTlem3VD  27676  csbeq2gVD  27681  csbunigVD  27687
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 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-v 2742  df-sbc 2936
  Copyright terms: Public domain W3C validator