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

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

Proof of Theorem alnex
StepHypRef Expression
1 fal 1294 . . . 4  |-  -. F.
21pm2.21i 608 . . 3  |-  ( F. 
->  A. x F.  )
3219.23h 1430 . 2  |-  ( A. x ( ph  -> F.  )  <->  ( E. x ph  -> F.  ) )
4 dfnot 1305 . . 3  |-  ( -. 
ph 
<->  ( ph  -> F.  ) )
54albii 1402 . 2  |-  ( A. x  -.  ph  <->  A. x ( ph  -> F.  ) )
6 dfnot 1305 . 2  |-  ( -. 
E. x ph  <->  ( E. x ph  -> F.  )
)
73, 5, 63bitr4i 210 1  |-  ( A. x  -.  ph  <->  -.  E. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 103   A.wal 1285   F. wfal 1292   E.wex 1424
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-5 1379  ax-gen 1381  ax-ie2 1426
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-fal 1293
This theorem is referenced by:  nex  1432  dfexdc  1433  exalim  1434  ax-9  1467  alinexa  1537  nexd  1547  alexdc  1553  19.30dc  1561  19.33b2  1563  alexnim  1582  ax6blem  1583  nf4dc  1603  nf4r  1604  mo2n  1973  notm0  3292  disjsn  3487  snprc  3490  dm0rn0  4621  reldm0  4622  dmsn0  4864  dmsn0el  4866  iotanul  4961  imadiflem  5058  imadif  5059  ltexprlemdisj  7109  recexprlemdisj  7133  fzo0  9507
  Copyright terms: Public domain W3C validator