Theorem alnex 1499

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 1501 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 1360	. . . 4 ⊢ ¬ ⊥
2	1	pm2.21i 646	. . 3 ⊢ (⊥ → ∀𝑥⊥)
3	2	19.23h 1498	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1371	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1470	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6		dfnot 1371	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
7	3, 5, 6	3bitr4i 212	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105  ∀wal 1351  ⊥wfal 1358  ∃wex 1492

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 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-ie2 1494

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-fal 1359

This theorem is referenced by:  nex  1500  dfexdc  1501  exalim  1502  ax-9  1531  alinexa  1603  nexd  1613  alexdc  1619  19.30dc  1627  19.33b2  1629  alexnim  1648  nnal  1649  ax6blem  1650  nf4dc  1670  nf4r  1671  mo2n  2054  notm0  3444  disjsn  3655  snprc  3658  dm0rn0  4845  reldm0  4846  dmsn0  5097  dmsn0el  5099  iotanul  5194  imadiflem  5296  imadif  5297  ltexprlemdisj  7605  recexprlemdisj  7629  fzo0  10168