Theorem alnex 1552

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 1554 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 1409	. . . 4 ⊢ ¬ ⊥
2	1	pm2.21i 655	. . 3 ⊢ (⊥ → ∀𝑥⊥)
3	2	19.23h 1551	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1420	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1523	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6		dfnot 1420	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
7	3, 5, 6	3bitr4i 212	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105  ∀wal 1400  ⊥wfal 1407  ∃wex 1545

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 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ie2 1547

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-fal 1408

This theorem is referenced by:  nex  1553  dfexdc  1554  exalim  1555  ax-9  1584  alinexa  1656  nexd  1666  alexdc  1672  19.30dc  1680  19.33b2  1682  alexnim  1701  nnal  1702  hbn  1703  nf4dc  1722  nf4r  1723  mo2n  2114  notm0  3542  disjsn  3767  snprc  3770  dm0rn0  4993  reldm0  4994  dmsn0  5250  dmsn0el  5252  iotanul  5348  imadiflem  5455  imadif  5456  ltexprlemdisj  7963  recexprlemdisj  7987  fzo0  10555