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

Step	Hyp	Ref	Expression
1		fal 1266	. . . 4 |- -. F.
2	1	pm2.21i 585	. . 3 |- ( F. -> A. x F. )
3	2	19.23h 1403	. 2 |- ( A. x ( ph -> F. ) <-> ( E. x ph -> F. ) )
4		dfnot 1278	. . 3 |- ( -. ph <-> ( ph -> F. ) )
5	4	albii 1375	. 2 |- ( A. x -. ph <-> A. x ( ph -> F. ) )
6		dfnot 1278	. 2 |- ( -. E. x ph <-> ( E. x ph -> F. ) )
7	3, 5, 6	3bitr4i 205	1 |- ( A. x -. ph <-> -. E. x ph )

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