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

Theorem spsbc 3782
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 2064 and rspsbc 3859. (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 2064 . . . 4 (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑)
2 sbsbc 3773 . . . 4 ([𝑦 / 𝑥]𝜑[𝑦 / 𝑥]𝜑)
31, 2sylib 219 . . 3 (∀𝑥𝜑[𝑦 / 𝑥]𝜑)
4 dfsbcq 3771 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
53, 4syl5ib 245 . 2 (𝑦 = 𝐴 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))
65vtocleg 3578 1 (𝐴𝑉 → (∀𝑥𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526   = wceq 1528  [wsb 2060  wcel 2105  [wsbc 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-sbc 3770
This theorem is referenced by:  spsbcd  3783  sbcth  3784  sbcthdv  3785  sbceqal  3832  sbcimdv  3840  csbiebt  3909  csbexg  5205  pm14.18  40637  sbcbi  40750  onfrALTlem3  40755  sbc3orgVD  41062  sbcbiVD  41087  csbingVD  41095  onfrALTlem3VD  41098  csbeq2gVD  41103  csbunigVD  41109
  Copyright terms: Public domain W3C validator