Theorem alnex 1522

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 1524 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 1380	. . . 4 |- -. F.
2	1	pm2.21i 647	. . 3 |- ( F. -> A. x F. )
3	2	19.23h 1521	. 2 |- ( A. x ( ph -> F. ) <-> ( E. x ph -> F. ) )
4		dfnot 1391	. . 3 |- ( -. ph <-> ( ph -> F. ) )
5	4	albii 1493	. 2 |- ( A. x -. ph <-> A. x ( ph -> F. ) )
6		dfnot 1391	. 2 |- ( -. E. x ph <-> ( E. x ph -> F. ) )
7	3, 5, 6	3bitr4i 212	1 |- ( A. x -. ph <-> -. E. x ph )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 105   A.wal 1371   F. wfal 1378   E.wex 1515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-5 1470  ax-gen 1472  ax-ie2 1517

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-fal 1379

This theorem is referenced by:  nex  1523  dfexdc  1524  exalim  1525  ax-9  1554  alinexa  1626  nexd  1636  alexdc  1642  19.30dc  1650  19.33b2  1652  alexnim  1671  nnal  1672  ax6blem  1673  nf4dc  1693  nf4r  1694  mo2n  2082  notm0  3481  disjsn  3695  snprc  3698  dm0rn0  4895  reldm0  4896  dmsn0  5150  dmsn0el  5152  iotanul  5247  imadiflem  5353  imadif  5354  ltexprlemdisj  7719  recexprlemdisj  7743  fzo0  10292