Theorem alnex 1523

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 1525 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 1380	. . . 4 ⊢ ¬ ⊥
2	1	pm2.21i 647	. . 3 ⊢ (⊥ → ∀𝑥⊥)
3	2	19.23h 1522	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1391	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1494	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6		dfnot 1391	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
7	3, 5, 6	3bitr4i 212	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105  ∀wal 1371  ⊥wfal 1378  ∃wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-5 1471  ax-gen 1473  ax-ie2 1518

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-fal 1379

This theorem is referenced by:  nex  1524  dfexdc  1525  exalim  1526  ax-9  1555  alinexa  1627  nexd  1637  alexdc  1643  19.30dc  1651  19.33b2  1653  alexnim  1672  nnal  1673  ax6blem  1674  nf4dc  1694  nf4r  1695  mo2n  2083  notm0  3485  disjsn  3700  snprc  3703  dm0rn0  4904  reldm0  4905  dmsn0  5159  dmsn0el  5161  iotanul  5256  imadiflem  5362  imadif  5363  ltexprlemdisj  7739  recexprlemdisj  7763  fzo0  10312