Theorem alnex 1510

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 1512 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 1371	. . . 4 |- -. F.
2	1	pm2.21i 647	. . 3 |- ( F. -> A. x F. )
3	2	19.23h 1509	. 2 |- ( A. x ( ph -> F. ) <-> ( E. x ph -> F. ) )
4		dfnot 1382	. . 3 |- ( -. ph <-> ( ph -> F. ) )
5	4	albii 1481	. 2 |- ( A. x -. ph <-> A. x ( ph -> F. ) )
6		dfnot 1382	. 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 1362   F. wfal 1369   E.wex 1503

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 1458  ax-gen 1460  ax-ie2 1505

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-fal 1370

This theorem is referenced by:  nex  1511  dfexdc  1512  exalim  1513  ax-9  1542  alinexa  1614  nexd  1624  alexdc  1630  19.30dc  1638  19.33b2  1640  alexnim  1659  nnal  1660  ax6blem  1661  nf4dc  1681  nf4r  1682  mo2n  2066  notm0  3458  disjsn  3669  snprc  3672  dm0rn0  4862  reldm0  4863  dmsn0  5114  dmsn0el  5116  iotanul  5211  imadiflem  5314  imadif  5315  ltexprlemdisj  7635  recexprlemdisj  7659  fzo0  10198