Theorem alnex 1492

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 1494 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.)

Assertion

Ref	Expression
alnex	⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Proof of Theorem alnex

Step	Hyp	Ref	Expression
1		fal 1355	. . . 4 ⊢ ¬ ⊥
2	1	pm2.21i 641	. . 3 ⊢ (⊥ → ∀𝑥⊥)
3	2	19.23h 1491	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1366	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1463	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6		dfnot 1366	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
7	3, 5, 6	3bitr4i 211	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104  ∀wal 1346  ⊥wfal 1353  ∃wex 1485

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 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-ie2 1487

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-fal 1354

This theorem is referenced by:  nex  1493  dfexdc  1494  exalim  1495  ax-9  1524  alinexa  1596  nexd  1606  alexdc  1612  19.30dc  1620  19.33b2  1622  alexnim  1641  nnal  1642  ax6blem  1643  nf4dc  1663  nf4r  1664  mo2n  2047  notm0  3435  disjsn  3645  snprc  3648  dm0rn0  4828  reldm0  4829  dmsn0  5078  dmsn0el  5080  iotanul  5175  imadiflem  5277  imadif  5278  ltexprlemdisj  7568  recexprlemdisj  7592  fzo0  10124