Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > spw | Structured version Visualization version Unicode version |
Description: Weak version of the specialization scheme sp 2053. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2053 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2053 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2012 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2053 are spfw 1965 (minimal distinct variable requirements), spnfw 1928 (when is not free in ), spvw 1898 (when does not appear in ), sptruw 1733 (when is true), and spfalw 1929 (when is false). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.) |
Ref | Expression |
---|---|
spw.1 |
Ref | Expression |
---|---|
spw |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1839 | . 2 | |
2 | ax-5 1839 | . 2 | |
3 | ax-5 1839 | . 2 | |
4 | spw.1 | . 2 | |
5 | 1, 2, 3, 4 | spfw 1965 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 wal 1481 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 |
This theorem is referenced by: hba1w 1974 hba1wOLD 1975 spaev 1978 ax12w 2010 bj-ssblem1 32630 bj-ax12w 32665 |
Copyright terms: Public domain | W3C validator |