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 1488 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 1349 | . . . 4 ⊢ ¬ ⊥ | |
2 | 1 | pm2.21i 636 | . . 3 ⊢ (⊥ → ∀𝑥⊥) |
3 | 2 | 19.23h 1485 | . 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥)) |
4 | dfnot 1360 | . . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥)) | |
5 | 4 | albii 1457 | . 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥)) |
6 | dfnot 1360 | . 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥)) | |
7 | 3, 5, 6 | 3bitr4i 211 | 1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 104 ∀wal 1340 ⊥wfal 1347 ∃wex 1479 |
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 604 ax-in2 605 ax-5 1434 ax-gen 1436 ax-ie2 1481 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-fal 1348 |
This theorem is referenced by: nex 1487 dfexdc 1488 exalim 1489 ax-9 1518 alinexa 1590 nexd 1600 alexdc 1606 19.30dc 1614 19.33b2 1616 alexnim 1635 nnal 1636 ax6blem 1637 nf4dc 1657 nf4r 1658 mo2n 2041 notm0 3424 disjsn 3632 snprc 3635 dm0rn0 4815 reldm0 4816 dmsn0 5065 dmsn0el 5067 iotanul 5162 imadiflem 5261 imadif 5262 ltexprlemdisj 7538 recexprlemdisj 7562 fzo0 10093 |
Copyright terms: Public domain | W3C validator |