Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  alnex GIF version

Theorem alnex 1476
 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 1478 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
StepHypRef Expression
1 fal 1339 . . . 4 ¬ ⊥
21pm2.21i 636 . . 3 (⊥ → ∀𝑥⊥)
3219.23h 1475 . 2 (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4 dfnot 1350 . . 3 𝜑 ↔ (𝜑 → ⊥))
54albii 1447 . 2 (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6 dfnot 1350 . 2 (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
73, 5, 63bitr4i 211 1 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104  ∀wal 1330  ⊥wfal 1337  ∃wex 1469 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 604  ax-in2 605  ax-5 1424  ax-gen 1426  ax-ie2 1471 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-fal 1338 This theorem is referenced by:  nex  1477  dfexdc  1478  exalim  1479  ax-9  1512  alinexa  1583  nexd  1593  alexdc  1599  19.30dc  1607  19.33b2  1609  alexnim  1628  ax6blem  1629  nf4dc  1649  nf4r  1650  mo2n  2028  notm0  3388  disjsn  3593  snprc  3596  dm0rn0  4764  reldm0  4765  dmsn0  5014  dmsn0el  5016  iotanul  5111  imadiflem  5210  imadif  5211  ltexprlemdisj  7439  recexprlemdisj  7463  fzo0  9977  bj-nnal  13121
 Copyright terms: Public domain W3C validator