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 2177. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2177 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2177 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2135 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2177 are spfw 2036 (minimal distinct variable requirements), spnfw 1980 (when 𝑥 is not free in ¬ 𝜑), spvw 1981 (when 𝑥 does not appear in 𝜑), sptruw 1803 (when 𝜑 is true), and spfalw 2000 (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 1907 | . 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) | |
2 | ax-5 1907 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) | |
3 | ax-5 1907 | . 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) | |
4 | spw.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
5 | 1, 2, 3, 4 | spfw 2036 | 1 ⊢ (∀𝑥𝜑 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∀wal 1531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1777 |
This theorem is referenced by: hba1w 2050 spaev 2053 ax12w 2133 bj-ssblem1 33982 bj-ax12w 34005 |
Copyright terms: Public domain | W3C validator |