Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > alnex | GIF version |
Description: Theorem 19.7 of [Margaris] p. 89. To read this intuitionistically, think of it as "if 𝜑 can be refuted for all 𝑥, then it is not possible to find an 𝑥 for which 𝜑 holds" (and likewise for the converse). Comparing this with dfexdc 1477 illustrates that statements which look similar (to someone used to classical logic) can be different intuitionistically due to different placement of negations. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 1-Feb-2015.) (Revised by Mario Carneiro, 12-May-2015.) |
Ref | Expression |
---|---|
alnex | ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fal 1338 | . . . 4 ⊢ ¬ ⊥ | |
2 | 1 | pm2.21i 635 | . . 3 ⊢ (⊥ → ∀𝑥⊥) |
3 | 2 | 19.23h 1474 | . 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥)) |
4 | dfnot 1349 | . . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥)) | |
5 | 4 | albii 1446 | . 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥)) |
6 | dfnot 1349 | . 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥)) | |
7 | 3, 5, 6 | 3bitr4i 211 | 1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 104 ∀wal 1329 ⊥wfal 1336 ∃wex 1468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-5 1423 ax-gen 1425 ax-ie2 1470 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-fal 1337 |
This theorem is referenced by: nex 1476 dfexdc 1477 exalim 1478 ax-9 1511 alinexa 1582 nexd 1592 alexdc 1598 19.30dc 1606 19.33b2 1608 alexnim 1627 ax6blem 1628 nf4dc 1648 nf4r 1649 mo2n 2025 notm0 3378 disjsn 3580 snprc 3583 dm0rn0 4751 reldm0 4752 dmsn0 5001 dmsn0el 5003 iotanul 5098 imadiflem 5197 imadif 5198 ltexprlemdisj 7407 recexprlemdisj 7431 fzo0 9938 bj-nnal 12938 |
Copyright terms: Public domain | W3C validator |