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

Theorem spsbc 3037
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 1996 and rspsbc 3103. (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 1996 . . . 4  |-  ( A. x ph  ->  [ y  /  x ] ph )
2 sbsbc 3029 . . . 4  |-  ( [ y  /  x ] ph 
<-> 
[. y  /  x ]. ph )
31, 2sylib 188 . . 3  |-  ( A. x ph  ->  [. y  /  x ]. ph )
4 dfsbcq 3027 . . 3  |-  ( y  =  A  ->  ( [. y  /  x ]. ph  <->  [. A  /  x ]. ph ) )
53, 4syl5ib 210 . 2  |-  ( y  =  A  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
65vtocleg 2888 1  |-  ( A  e.  V  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1531    = wceq 1633   [wsb 1639    e. wcel 1701   [.wsbc 3025
This theorem is referenced by:  spsbcd  3038  sbcth  3039  sbcthdv  3040  sbceqal  3076  sbcimdv  3086  csbexg  3125  csbiebt  3151  ovmpt2dxf  6015  pm14.18  26776  sbcbi  27797  onfrALTlem3  27803  csbeq2g  27809  sbc3orgVD  28138  sbcbiVD  28163  csbingVD  28171  onfrALTlem3VD  28174  csbeq2gVD  28179  csbunigVD  28185
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1533  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-v 2824  df-sbc 3026
  Copyright terms: Public domain W3C validator