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

Theorem spsbc 3003
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 1964 and rspsbc 3069. (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 1964 . . . 4  |-  ( A. x ph  ->  [ y  /  x ] ph )
2 sbsbc 2995 . . . 4  |-  ( [ y  /  x ] ph 
<-> 
[. y  /  x ]. ph )
31, 2sylib 188 . . 3  |-  ( A. x ph  ->  [. y  /  x ]. ph )
4 dfsbcq 2993 . . 3  |-  ( y  =  A  ->  ( [. y  /  x ]. ph  <->  [. A  /  x ]. ph ) )
53, 4syl5ib 210 . 2  |-  ( y  =  A  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
65vtocleg 2854 1  |-  ( A  e.  V  ->  ( A. x ph  ->  [. A  /  x ]. ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527    = wceq 1623   [wsb 1629    e. wcel 1684   [.wsbc 2991
This theorem is referenced by:  spsbcd  3004  sbcth  3005  sbcthdv  3006  sbceqal  3042  sbcimdv  3052  csbexg  3091  csbiebt  3117  ovmpt2dxf  5973  pm14.18  27628  sbcbi  28303  onfrALTlem3  28309  csbeq2g  28315  sbc3orgVD  28627  sbcbiVD  28652  csbingVD  28660  onfrALTlem3VD  28663  csbeq2gVD  28668  csbunigVD  28674
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790  df-sbc 2992
  Copyright terms: Public domain W3C validator