Theorem alnex 1443

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 1445 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 1306	. . . 4 ⊢ ¬ ⊥
2	1	pm2.21i 615	. . 3 ⊢ (⊥ → ∀𝑥⊥)
3	2	19.23h 1442	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1317	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1414	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6		dfnot 1317	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
7	3, 5, 6	3bitr4i 211	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104  ∀wal 1297  ⊥wfal 1304  ∃wex 1436

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-5 1391  ax-gen 1393  ax-ie2 1438

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-fal 1305

This theorem is referenced by:  nex  1444  dfexdc  1445  exalim  1446  ax-9  1479  alinexa  1550  nexd  1560  alexdc  1566  19.30dc  1574  19.33b2  1576  alexnim  1595  ax6blem  1596  nf4dc  1616  nf4r  1617  mo2n  1988  notm0  3330  disjsn  3532  snprc  3535  dm0rn0  4694  reldm0  4695  dmsn0  4942  dmsn0el  4944  iotanul  5039  imadiflem  5138  imadif  5139  ltexprlemdisj  7315  recexprlemdisj  7339  fzo0  9786