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

Theorem alnex 1476
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 1478 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 1339 . . . 4  |-  -. F.
21pm2.21i 636 . . 3  |-  ( F. 
->  A. x F.  )
3219.23h 1475 . 2  |-  ( A. x ( ph  -> F.  )  <->  ( E. x ph  -> F.  ) )
4 dfnot 1350 . . 3  |-  ( -. 
ph 
<->  ( ph  -> F.  ) )
54albii 1447 . 2  |-  ( A. x  -.  ph  <->  A. x ( ph  -> F.  ) )
6 dfnot 1350 . 2  |-  ( -. 
E. x ph  <->  ( E. x ph  -> F.  )
)
73, 5, 63bitr4i 211 1  |-  ( A. x  -.  ph  <->  -.  E. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 104   A.wal 1330   F. wfal 1337   E.wex 1469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1424  ax-gen 1426  ax-ie2 1471
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-fal 1338
This theorem is referenced by:  nex  1477  dfexdc  1478  exalim  1479  ax-9  1512  alinexa  1583  nexd  1593  alexdc  1599  19.30dc  1607  19.33b2  1609  alexnim  1628  ax6blem  1629  nf4dc  1649  nf4r  1650  mo2n  2028  notm0  3387  disjsn  3592  snprc  3595  dm0rn0  4763  reldm0  4764  dmsn0  5013  dmsn0el  5015  iotanul  5110  imadiflem  5209  imadif  5210  ltexprlemdisj  7437  recexprlemdisj  7461  fzo0  9975  bj-nnal  13118
  Copyright terms: Public domain W3C validator