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

Theorem spw 1702
 Description: Weak version of specialization scheme sp 1759. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 1759 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 1759 having no wff metavariables and mutually distinct set variables (see ax11wdemo 1734 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 1759 are spfw 1699 (minimal distinct variable requirements), spnfw 1678 (when is not free in ), spvw 1674 (when does not appear in ), sptruw 1679 (when is true), and spfalw 1680 (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-17 1623 . 2
2 ax-17 1623 . 2
3 ax-17 1623 . 2
4 spw.1 . 2
51, 2, 3, 4spfw 1699 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177  wal 1546 This theorem is referenced by:  spvwOLD  1704  spfalwOLD  1708  hba1w  1718  ax11w  1732 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548
 Copyright terms: Public domain W3C validator