![]() |
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 2207. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2207 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2207 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2167 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2207 are spfw 2121 (minimal distinct variable requirements), spnfw 2086 (when 𝑥 is not free in ¬ 𝜑), spvw 2067 (when 𝑥 does not appear in 𝜑), sptruw 1881 (when 𝜑 is true), and spfalw 2087 (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 1991 | . 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) | |
2 | ax-5 1991 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) | |
3 | ax-5 1991 | . 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) | |
4 | spw.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
5 | 1, 2, 3, 4 | spfw 2121 | 1 ⊢ (∀𝑥𝜑 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∀wal 1629 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 |
This theorem is referenced by: hba1w 2131 hba1wOLD 2132 spaev 2135 ax12w 2165 bj-ssblem1 32968 bj-ax12w 33002 |
Copyright terms: Public domain | W3C validator |