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

Theorem spsbc 3173
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 2091 and rspsbc 3239. (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 2091 . . . 4  |-  ( A. x ph  ->  [ y  /  x ] ph )
2 sbsbc 3165 . . . 4  |-  ( [ y  /  x ] ph 
<-> 
[. y  /  x ]. ph )
31, 2sylib 189 . . 3  |-  ( A. x ph  ->  [. y  /  x ]. ph )
4 dfsbcq 3163 . . 3  |-  ( y  =  A  ->  ( [. y  /  x ]. ph  <->  [. A  /  x ]. ph ) )
53, 4syl5ib 211 . 2  |-  ( y  =  A  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
65vtocleg 3022 1  |-  ( A  e.  V  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549    = wceq 1652   [wsb 1658    e. wcel 1725   [.wsbc 3161
This theorem is referenced by:  spsbcd  3174  sbcth  3175  sbcthdv  3176  sbceqal  3212  sbcimdv  3222  csbexg  3261  csbiebt  3287  pm14.18  27605  sbcbi  28624  onfrALTlem3  28630  csbeq2g  28636  sbc3orgVD  28963  sbcbiVD  28988  csbingVD  28996  onfrALTlem3VD  28999  csbeq2gVD  29004  csbunigVD  29010
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-v 2958  df-sbc 3162
  Copyright terms: Public domain W3C validator