Theorem alnex 1497

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 1499 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 1496	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1371	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1468	. 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 1490

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 1445  ax-gen 1447  ax-ie2 1492

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

This theorem is referenced by:  nex  1498  dfexdc  1499  exalim  1500  ax-9  1529  alinexa  1601  nexd  1611  alexdc  1617  19.30dc  1625  19.33b2  1627  alexnim  1646  nnal  1647  ax6blem  1648  nf4dc  1668  nf4r  1669  mo2n  2052  notm0  3441  disjsn  3651  snprc  3654  dm0rn0  4837  reldm0  4838  dmsn0  5088  dmsn0el  5090  iotanul  5185  imadiflem  5287  imadif  5288  ltexprlemdisj  7580  recexprlemdisj  7604  fzo0  10138