Theorem alnex 1475

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 1477 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 1338	. . . 4 ⊢ ¬ ⊥
2	1	pm2.21i 635	. . 3 ⊢ (⊥ → ∀𝑥⊥)
3	2	19.23h 1474	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1349	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1446	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6		dfnot 1349	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
7	3, 5, 6	3bitr4i 211	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104  ∀wal 1329  ⊥wfal 1336  ∃wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-5 1423  ax-gen 1425  ax-ie2 1470

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-fal 1337

This theorem is referenced by:  nex  1476  dfexdc  1477  exalim  1478  ax-9  1511  alinexa  1582  nexd  1592  alexdc  1598  19.30dc  1606  19.33b2  1608  alexnim  1627  ax6blem  1628  nf4dc  1648  nf4r  1649  mo2n  2027  notm0  3383  disjsn  3585  snprc  3588  dm0rn0  4756  reldm0  4757  dmsn0  5006  dmsn0el  5008  iotanul  5103  imadiflem  5202  imadif  5203  ltexprlemdisj  7414  recexprlemdisj  7438  fzo0  9945  bj-nnal  12949