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

Theorem spsbc 3414
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 2340 and rspsbc 3483. (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 2340 . . . 4 (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑)
2 sbsbc 3405 . . . 4 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
31, 2sylib 206 . . 3 (∀𝑥𝜑[𝑦 / 𝑥]𝜑)
4 dfsbcq 3403 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
53, 4syl5ib 232 . 2 (𝑦 = 𝐴 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))
65vtocleg 3251 1 (𝐴𝑉 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472   = wceq 1474  [wsb 1866  wcel 1976  [wsbc 3401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-v 3174  df-sbc 3402
This theorem is referenced by:  spsbcd  3415  sbcth  3416  sbcthdv  3417  sbceqal  3453  sbcimdv  3464  sbcimdvOLD  3465  csbiebt  3518  csbexg  4715  pm14.18  37454  sbcbi  37573  onfrALTlem3  37583  csbeq2gOLD  37589  sbc3orgVD  37911  sbcbiVD  37937  csbingVD  37945  onfrALTlem3VD  37948  csbeq2gVD  37953  csbunigVD  37959
  Copyright terms: Public domain W3C validator