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

Theorem spsbc 3079
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 2029 and rspsbc 3145. (Contributed by NM, 16-Jan-2004.)
Assertion
Ref Expression
spsbc  |-  ( A  e.  V  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)

Proof of Theorem spsbc
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 stdpc4 2029 . . . 4  |-  ( A. x ph  ->  [ y  /  x ] ph )
2 sbsbc 3071 . . . 4  |-  ( [ y  /  x ] ph 
<-> 
[. y  /  x ]. ph )
31, 2sylib 188 . . 3  |-  ( A. x ph  ->  [. y  /  x ]. ph )
4 dfsbcq 3069 . . 3  |-  ( y  =  A  ->  ( [. y  /  x ]. ph  <->  [. A  /  x ]. ph ) )
53, 4syl5ib 210 . 2  |-  ( y  =  A  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
65vtocleg 2930 1  |-  ( A  e.  V  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1540    = wceq 1642   [wsb 1648    e. wcel 1710   [.wsbc 3067
This theorem is referenced by:  spsbcd  3080  sbcth  3081  sbcthdv  3082  sbceqal  3118  sbcimdv  3128  csbexg  3167  csbiebt  3193  ovmpt2dxf  6057  pm14.18  26951  sbcbi  28031  onfrALTlem3  28037  csbeq2g  28043  sbc3orgVD  28372  sbcbiVD  28397  csbingVD  28405  onfrALTlem3VD  28408  csbeq2gVD  28413  csbunigVD  28419
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-v 2866  df-sbc 3068
  Copyright terms: Public domain W3C validator