Theorem alnex 1547

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 1549 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 1404	. . . 4 ⊢ ¬ ⊥
2	1	pm2.21i 651	. . 3 ⊢ (⊥ → ∀𝑥⊥)
3	2	19.23h 1546	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1415	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1518	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6		dfnot 1415	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
7	3, 5, 6	3bitr4i 212	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105  ∀wal 1395  ⊥wfal 1402  ∃wex 1540

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 619  ax-in2 620  ax-5 1495  ax-gen 1497  ax-ie2 1542

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-fal 1403

This theorem is referenced by:  nex  1548  dfexdc  1549  exalim  1550  ax-9  1579  alinexa  1651  nexd  1661  alexdc  1667  19.30dc  1675  19.33b2  1677  alexnim  1696  nnal  1697  ax6blem  1698  nf4dc  1718  nf4r  1719  mo2n  2107  notm0  3515  disjsn  3731  snprc  3734  dm0rn0  4948  reldm0  4949  dmsn0  5204  dmsn0el  5206  iotanul  5302  imadiflem  5409  imadif  5410  ltexprlemdisj  7825  recexprlemdisj  7849  fzo0  10404