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

Theorem a4sbc 2964
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 3030. (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 2956 . . . 4  |-  ( [ y  /  x ] ph 
<-> 
[. y  /  x ]. ph )
31, 2sylib 190 . . 3  |-  ( A. x ph  ->  [. y  /  x ]. ph )
4 dfsbcq 2954 . . 3  |-  ( y  =  A  ->  ( [. y  /  x ]. ph  <->  [. A  /  x ]. ph ) )
53, 4syl5ib 212 . 2  |-  ( y  =  A  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
65vtocleg 2822 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 2952
This theorem is referenced by:  a4sbcd  2965  sbcth  2966  sbcthdv  2967  sbceqal  3003  sbcimdv  3013  csbexg  3052  csbiebt  3078  ovmpt2dxf  5893  pm14.18  26982  sbcbi  27340  onfrALTlem3  27346  csbeq2g  27352  sbc3orgVD  27661  sbcbiVD  27686  csbingVD  27694  onfrALTlem3VD  27697  csbeq2gVD  27702  csbunigVD  27708
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 2759  df-sbc 2953
  Copyright terms: Public domain W3C validator