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

Theorem alnex 1388
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 1390 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 1250 . . . 4 ¬ ⊥
21pm2.21i 575 . . 3 (⊥ → ∀𝑥⊥)
3219.23h 1387 . 2 (∀𝑥(𝜑 → ⊥) ↔ (∃𝑥𝜑 → ⊥))
4 dfnot 1262 . . 3 𝜑 ↔ (𝜑 → ⊥))
54albii 1359 . 2 (∀𝑥 ¬ 𝜑 ↔ ∀𝑥(𝜑 → ⊥))
6 dfnot 1262 . 2 (¬ ∃𝑥𝜑 ↔ (∃𝑥𝜑 → ⊥))
73, 5, 63bitr4i 201 1 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 98  wal 1241  wfal 1248  wex 1381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-5 1336  ax-gen 1338  ax-ie2 1383
This theorem depends on definitions:  df-bi 110  df-tru 1246  df-fal 1249
This theorem is referenced by:  nex  1389  dfexdc  1390  exalim  1391  ax-9  1424  alinexa  1494  nexd  1504  alexdc  1510  19.30dc  1518  19.33b2  1520  alexnim  1539  ax6blem  1540  nf4dc  1560  nf4r  1561  mo2n  1928  disjsn  3432  snprc  3435  dm0rn0  4552  reldm0  4553  dmsn0  4788  dmsn0el  4790  iotanul  4882  imadiflem  4978  imadif  4979  ltexprlemdisj  6704  recexprlemdisj  6728  fzo0  9024
  Copyright terms: Public domain W3C validator