Theorem alnex 1475

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 1477 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 1338	. . . 4 |- -. F.
2	1	pm2.21i 635	. . 3 |- ( F. -> A. x F. )
3	2	19.23h 1474	. 2 |- ( A. x ( ph -> F. ) <-> ( E. x ph -> F. ) )
4		dfnot 1349	. . 3 |- ( -. ph <-> ( ph -> F. ) )
5	4	albii 1446	. 2 |- ( A. x -. ph <-> A. x ( ph -> F. ) )
6		dfnot 1349	. 2 |- ( -. E. x ph <-> ( E. x ph -> F. ) )
7	3, 5, 6	3bitr4i 211	1 |- ( A. x -. ph <-> -. E. x ph )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104   A.wal 1329   F. wfal 1336   E.wex 1468

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 603  ax-in2 604  ax-5 1423  ax-gen 1425  ax-ie2 1470

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-fal 1337

This theorem is referenced by:  nex  1476  dfexdc  1477  exalim  1478  ax-9  1511  alinexa  1582  nexd  1592  alexdc  1598  19.30dc  1606  19.33b2  1608  alexnim  1627  ax6blem  1628  nf4dc  1648  nf4r  1649  mo2n  2025  notm0  3378  disjsn  3580  snprc  3583  dm0rn0  4751  reldm0  4752  dmsn0  5001  dmsn0el  5003  iotanul  5098  imadiflem  5197  imadif  5198  ltexprlemdisj  7407  recexprlemdisj  7431  fzo0  9938  bj-nnal  12938