![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > spw | Structured version Visualization version GIF version |
Description: Weak version of the specialization scheme sp 2175. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2175 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2175 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2130 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2175 are spfw 2035 (minimal distinct variable requirements), spnfw 1982 (when 𝑥 is not free in ¬ 𝜑), spvw 1983 (when 𝑥 does not appear in 𝜑), sptruw 1807 (when 𝜑 is true), spfalw 2000 (when 𝜑 is false), and spvv 1999 (where 𝜑 is changed into 𝜓). (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 1912 | . 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) | |
2 | ax-5 1912 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) | |
3 | ax-5 1912 | . 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) | |
4 | spw.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
5 | 1, 2, 3, 4 | spfw 2035 | 1 ⊢ (∀𝑥𝜑 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∀wal 1538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 |
This theorem is referenced by: hba1w 2049 19.8aw 2052 exexw 2053 spaev 2054 ax12w 2128 nfcriOLD 2892 rspw 3232 reldisj 4451 ralidmw 4507 dtruALT2 5368 dtruOLD 5441 bj-ssblem1 35847 bj-ax12w 35870 |
Copyright terms: Public domain | W3C validator |