Theorem alnex 1487

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 1489 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 1350	. . . 4 ⊢ ¬ ⊥
2	1	pm2.21i 636	. . 3 ⊢ (⊥ → ∀𝑥⊥)
3	2	19.23h 1486	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1361	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1458	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6		dfnot 1361	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
7	3, 5, 6	3bitr4i 211	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104  ∀wal 1341  ⊥wfal 1348  ∃wex 1480

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 1435  ax-gen 1437  ax-ie2 1482

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-fal 1349

This theorem is referenced by:  nex  1488  dfexdc  1489  exalim  1490  ax-9  1519  alinexa  1591  nexd  1601  alexdc  1607  19.30dc  1615  19.33b2  1617  alexnim  1636  nnal  1637  ax6blem  1638  nf4dc  1658  nf4r  1659  mo2n  2042  notm0  3429  disjsn  3638  snprc  3641  dm0rn0  4821  reldm0  4822  dmsn0  5071  dmsn0el  5073  iotanul  5168  imadiflem  5267  imadif  5268  ltexprlemdisj  7547  recexprlemdisj  7571  fzo0  10103