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

Theorem spw 1861
 Description: Weak version of the specialization scheme sp 1914. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 1914 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 1914 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 1885 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 1914 are spfw 1860 (minimal distinct variable requirements), spnfw 1837 (when is not free in ), spvw 1807 (when does not appear in ), sptruw 1675 (when is true), and spfalw 1838 (when is false). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.)
Hypothesis
Ref Expression
spw.1
Assertion
Ref Expression
spw
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem spw
StepHypRef Expression
1 ax-5 1752 . 2
2 ax-5 1752 . 2
3 ax-5 1752 . 2
4 spw.1 . 2
51, 2, 3, 4spfw 1860 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187  wal 1435 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843 This theorem depends on definitions:  df-bi 188  df-ex 1658 This theorem is referenced by:  hba1w  1868  ax12w  1883  bj-ax12w  31236
 Copyright terms: Public domain W3C validator