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

Theorem spw 1660
 Description: Weak version of specialization scheme sp 1716. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 1716 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 1716 having no wff metavariables and mutually distinct set variables (see ax11wdemo 1697 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 1716 are spfw 1657 (minimal distinct variable requirements), spnfw 1640 (when is not free in ), spvw 1661 (when does not appear in ), sptruw 1669 (when is true), and spfalw 1670 (when is false). (Contributed by NM, 9-Apr-2017.)
Hypothesis
Ref Expression
spw.1
Assertion
Ref Expression
spw
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem spw
StepHypRef Expression
1 ax-17 1603 . . 3
2 ax-5 1544 . . 3
3 spw.1 . . . . . 6
43biimprd 214 . . . . 5
54equcoms 1651 . . . 4
65spimvw 1639 . . 3
71, 2, 6syl56 30 . 2
83biimpd 198 . . 3
98spimvw 1639 . 2
107, 9mpg 1535 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176  wal 1527 This theorem is referenced by:  spvw  1661  spfalw  1670  hba1w  1681  ax11w  1695 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529
 Copyright terms: Public domain W3C validator