Theorem alnex 1545

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 1547 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 1402	. . . 4 ⊢ ¬ ⊥
2	1	pm2.21i 649	. . 3 ⊢ (⊥ → ∀𝑥⊥)
3	2	19.23h 1544	. 2 ⊢ (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4		dfnot 1413	. . 3 ⊢ (¬ 𝜑 ↔ (𝜑 → ⊥))
5	4	albii 1516	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6		dfnot 1413	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
7	3, 5, 6	3bitr4i 212	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

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

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-ie2 1540

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-fal 1401

This theorem is referenced by:  nex  1546  dfexdc  1547  exalim  1548  ax-9  1577  alinexa  1649  nexd  1659  alexdc  1665  19.30dc  1673  19.33b2  1675  alexnim  1694  nnal  1695  ax6blem  1696  nf4dc  1716  nf4r  1717  mo2n  2105  notm0  3512  disjsn  3728  snprc  3731  dm0rn0  4939  reldm0  4940  dmsn0  5195  dmsn0el  5197  iotanul  5293  imadiflem  5399  imadif  5400  ltexprlemdisj  7789  recexprlemdisj  7813  fzo0  10362