Theorem alnex 1510

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 1512 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 1509	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1382	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1481	. 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 1503

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 1458  ax-gen 1460  ax-ie2 1505

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

This theorem is referenced by:  nex  1511  dfexdc  1512  exalim  1513  ax-9  1542  alinexa  1614  nexd  1624  alexdc  1630  19.30dc  1638  19.33b2  1640  alexnim  1659  nnal  1660  ax6blem  1661  nf4dc  1681  nf4r  1682  mo2n  2070  notm0  3467  disjsn  3680  snprc  3683  dm0rn0  4879  reldm0  4880  dmsn0  5133  dmsn0el  5135  iotanul  5230  imadiflem  5333  imadif  5334  ltexprlemdisj  7666  recexprlemdisj  7690  fzo0  10235