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

Theorem spsbc 3165
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 2087 and rspsbc 3231. (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 2087 . . . 4  |-  ( A. x ph  ->  [ y  /  x ] ph )
2 sbsbc 3157 . . . 4  |-  ( [ y  /  x ] ph 
<-> 
[. y  /  x ]. ph )
31, 2sylib 189 . . 3  |-  ( A. x ph  ->  [. y  /  x ]. ph )
4 dfsbcq 3155 . . 3  |-  ( y  =  A  ->  ( [. y  /  x ]. ph  <->  [. A  /  x ]. ph ) )
53, 4syl5ib 211 . 2  |-  ( y  =  A  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
65vtocleg 3014 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 3153
This theorem is referenced by:  spsbcd  3166  sbcth  3167  sbcthdv  3168  sbceqal  3204  sbcimdv  3214  csbexg  3253  csbiebt  3279  pm14.18  27596  sbcbi  28561  onfrALTlem3  28567  csbeq2g  28573  sbc3orgVD  28900  sbcbiVD  28925  csbingVD  28933  onfrALTlem3VD  28936  csbeq2gVD  28941  csbunigVD  28947
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 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-v 2950  df-sbc 3154
  Copyright terms: Public domain W3C validator