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

Theorem spsbc 3481
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. This is Frege's ninth axiom per Proposition 58 of [Frege1879] p. 51. See also stdpc4 2381 and rspsbc 3551. (Contributed by NM, 16-Jan-2004.)
Assertion
Ref Expression
spsbc (𝐴𝑉 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))

Proof of Theorem spsbc
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 stdpc4 2381 . . . 4 (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑)
2 sbsbc 3472 . . . 4 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
31, 2sylib 208 . . 3 (∀𝑥𝜑[𝑦 / 𝑥]𝜑)
4 dfsbcq 3470 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
53, 4syl5ib 234 . 2 (𝑦 = 𝐴 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))
65vtocleg 3310 1 (𝐴𝑉 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521   = wceq 1523  [wsb 1937  wcel 2030  [wsbc 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233  df-sbc 3469
This theorem is referenced by:  spsbcd  3482  sbcth  3483  sbcthdv  3484  sbceqal  3520  sbcimdv  3531  sbcimdvOLD  3532  csbiebt  3586  csbexg  4825  pm14.18  38946  sbcbi  39066  onfrALTlem3  39076  csbeq2gOLD  39082  sbc3orgVD  39400  sbcbiVD  39426  csbingVD  39434  onfrALTlem3VD  39437  csbeq2gVD  39442  csbunigVD  39448
  Copyright terms: Public domain W3C validator