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

Theorem alnex 1320
Description: Theorem 19.7 of [Margaris] p. 89. To read this intuitionistically, think of it as "if φ can be refuted for all x, then it is not possible to find an x for which φ holds" (and likewise for the converse). Comparing this with df-ex 1758 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 (x ¬ φ ↔ ¬ xφ)

Proof of Theorem alnex
StepHypRef Expression
1 fal 1204 . . . 4 ¬ ⊥
21pm2.21i 553 . . 3 ( ⊥ → x ⊥ )
3219.23 1319 . 2 (x(φ → ⊥ ) ↔ (xφ → ⊥ ))
4 dfnot 1214 . . 3 φ ↔ (φ → ⊥ ))
54albii 1290 . 2 (x ¬ φx(φ → ⊥ ))
6 dfnot 1214 . 2 xφ ↔ (xφ → ⊥ ))
73, 5, 63bitr4i 199 1 (x ¬ φ ↔ ¬ xφ)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 96  wfal 1199  wal 1266  wex 1313
This theorem is referenced by:  nex  1321  dfexdc  1322  ax-9  1354  alinexa  1412  nexd  1419  19.33b2  1430  ax6blem  1441  df-ex  1758  alex  1759  19.35  1763  mo  1782  mo2  1789  2mo  1839  alexn  1877  nf4  1891  a12lem2  1933
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-in1 526  ax-in2 527  ax-5 1267  ax-gen 1269  ax-ie2 1315
This theorem depends on definitions:  df-bi 108  df-tru 1201  df-fal 1202
  Copyright terms: Public domain W3C validator