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

Theorem alnex 1510
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 1512 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 1371 . . . 4  |-  -. F.
21pm2.21i 647 . . 3  |-  ( F. 
->  A. x F.  )
3219.23h 1509 . 2  |-  ( A. x ( ph  -> F.  )  <->  ( E. x ph  -> F.  ) )
4 dfnot 1382 . . 3  |-  ( -. 
ph 
<->  ( ph  -> F.  ) )
54albii 1481 . 2  |-  ( A. x  -.  ph  <->  A. x ( ph  -> F.  ) )
6 dfnot 1382 . 2  |-  ( -. 
E. x ph  <->  ( E. x ph  -> F.  )
)
73, 5, 63bitr4i 212 1  |-  ( A. x  -.  ph  <->  -.  E. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 105   A.wal 1362   F. wfal 1369   E.wex 1503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-5 1458  ax-gen 1460  ax-ie2 1505
This theorem depends on definitions:  df-bi 117  df-tru 1367  df-fal 1370
This theorem is referenced by:  nex  1511  dfexdc  1512  exalim  1513  ax-9  1542  alinexa  1614  nexd  1624  alexdc  1630  19.30dc  1638  19.33b2  1640  alexnim  1659  nnal  1660  ax6blem  1661  nf4dc  1681  nf4r  1682  mo2n  2066  notm0  3458  disjsn  3669  snprc  3672  dm0rn0  4862  reldm0  4863  dmsn0  5114  dmsn0el  5116  iotanul  5211  imadiflem  5314  imadif  5315  ltexprlemdisj  7635  recexprlemdisj  7659  fzo0  10198
  Copyright terms: Public domain W3C validator