Theorem alnex 1521

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 1523 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 1379	. . . 4 ⊢ ¬ ⊥
2	1	pm2.21i 647	. . 3 ⊢ (⊥ → ∀𝑥⊥)
3	2	19.23h 1520	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1390	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1492	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6		dfnot 1390	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
7	3, 5, 6	3bitr4i 212	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105  ∀wal 1370  ⊥wfal 1377  ∃wex 1514

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 1469  ax-gen 1471  ax-ie2 1516

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-fal 1378

This theorem is referenced by:  nex  1522  dfexdc  1523  exalim  1524  ax-9  1553  alinexa  1625  nexd  1635  alexdc  1641  19.30dc  1649  19.33b2  1651  alexnim  1670  nnal  1671  ax6blem  1672  nf4dc  1692  nf4r  1693  mo2n  2081  notm0  3480  disjsn  3694  snprc  3697  dm0rn0  4894  reldm0  4895  dmsn0  5149  dmsn0el  5151  iotanul  5246  imadiflem  5352  imadif  5353  ltexprlemdisj  7718  recexprlemdisj  7742  fzo0  10290