Theorem alnex 1428

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 1430 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

Step	Hyp	Ref	Expression
1		fal 1291	. . . 4 |- -. F.
2	1	pm2.21i 607	. . 3 |- ( F. -> A. x F. )
3	2	19.23h 1427	. 2 |- ( A. x ( ph -> F. ) <-> ( E. x ph -> F. ) )
4		dfnot 1302	. . 3 |- ( -. ph <-> ( ph -> F. ) )
5	4	albii 1399	. 2 |- ( A. x -. ph <-> A. x ( ph -> F. ) )
6		dfnot 1302	. 2 |- ( -. E. x ph <-> ( E. x ph -> F. ) )
7	3, 5, 6	3bitr4i 210	1 |- ( A. x -. ph <-> -. E. x ph )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 103   A.wal 1282   F. wfal 1289   E.wex 1421

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 576  ax-in2 577  ax-5 1376  ax-gen 1378  ax-ie2 1423

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-fal 1290

This theorem is referenced by:  nex  1429  dfexdc  1430  exalim  1431  ax-9  1464  alinexa  1534  nexd  1544  alexdc  1550  19.30dc  1558  19.33b2  1560  alexnim  1579  ax6blem  1580  nf4dc  1600  nf4r  1601  mo2n  1969  disjsn  3454  snprc  3457  dm0rn0  4570  reldm0  4571  dmsn0  4808  dmsn0el  4810  iotanul  4902  imadiflem  4998  imadif  4999  ltexprlemdisj  6796  recexprlemdisj  6820  fzo0  9177