Theorem alnex 1513

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 1515 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 1371	. . . 4 ⊢ ¬ ⊥
2	1	pm2.21i 647	. . 3 ⊢ (⊥ → ∀𝑥⊥)
3	2	19.23h 1512	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1382	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1484	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6		dfnot 1382	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
7	3, 5, 6	3bitr4i 212	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105  ∀wal 1362  ⊥wfal 1369  ∃wex 1506

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 1461  ax-gen 1463  ax-ie2 1508

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-fal 1370

This theorem is referenced by:  nex  1514  dfexdc  1515  exalim  1516  ax-9  1545  alinexa  1617  nexd  1627  alexdc  1633  19.30dc  1641  19.33b2  1643  alexnim  1662  nnal  1663  ax6blem  1664  nf4dc  1684  nf4r  1685  mo2n  2073  notm0  3471  disjsn  3684  snprc  3687  dm0rn0  4883  reldm0  4884  dmsn0  5137  dmsn0el  5139  iotanul  5234  imadiflem  5337  imadif  5338  ltexprlemdisj  7673  recexprlemdisj  7697  fzo0  10244