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

Theorem alnex 1404
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 1406 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 1266 . . . 4  |-  -. F.
21pm2.21i 585 . . 3  |-  ( F. 
->  A. x F.  )
3219.23h 1403 . 2  |-  ( A. x ( ph  -> F.  )  <->  ( E. x ph  -> F.  ) )
4 dfnot 1278 . . 3  |-  ( -. 
ph 
<->  ( ph  -> F.  ) )
54albii 1375 . 2  |-  ( A. x  -.  ph  <->  A. x ( ph  -> F.  ) )
6 dfnot 1278 . 2  |-  ( -. 
E. x ph  <->  ( E. x ph  -> F.  )
)
73, 5, 63bitr4i 205 1  |-  ( A. x  -.  ph  <->  -.  E. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 102   A.wal 1257   F. wfal 1264   E.wex 1397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-5 1352  ax-gen 1354  ax-ie2 1399
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-fal 1265
This theorem is referenced by:  nex  1405  dfexdc  1406  exalim  1407  ax-9  1440  alinexa  1510  nexd  1520  alexdc  1526  19.30dc  1534  19.33b2  1536  alexnim  1555  ax6blem  1556  nf4dc  1576  nf4r  1577  mo2n  1944  disjsn  3459  snprc  3462  dm0rn0  4579  reldm0  4580  dmsn0  4815  dmsn0el  4817  iotanul  4909  imadiflem  5005  imadif  5006  ltexprlemdisj  6761  recexprlemdisj  6785  fzo0  9125
  Copyright terms: Public domain W3C validator