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

Theorem alnex 1429
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 1431 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 1292 . . . 4  |-  -. F.
21pm2.21i 608 . . 3  |-  ( F. 
->  A. x F.  )
3219.23h 1428 . 2  |-  ( A. x ( ph  -> F.  )  <->  ( E. x ph  -> F.  ) )
4 dfnot 1303 . . 3  |-  ( -. 
ph 
<->  ( ph  -> F.  ) )
54albii 1400 . 2  |-  ( A. x  -.  ph  <->  A. x ( ph  -> F.  ) )
6 dfnot 1303 . 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 1283   F. wfal 1290   E.wex 1422
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 1377  ax-gen 1379  ax-ie2 1424
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-fal 1291
This theorem is referenced by:  nex  1430  dfexdc  1431  exalim  1432  ax-9  1465  alinexa  1535  nexd  1545  alexdc  1551  19.30dc  1559  19.33b2  1561  alexnim  1580  ax6blem  1581  nf4dc  1601  nf4r  1602  mo2n  1971  disjsn  3472  snprc  3475  dm0rn0  4600  reldm0  4601  dmsn0  4838  dmsn0el  4840  iotanul  4932  imadiflem  5029  imadif  5030  ltexprlemdisj  6928  recexprlemdisj  6952  fzo0  9324
  Copyright terms: Public domain W3C validator