Theorem alnex 1548

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 1550 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 1405	. . . 4 |- -. F.
2	1	pm2.21i 651	. . 3 |- ( F. -> A. x F. )
3	2	19.23h 1547	. 2 |- ( A. x ( ph -> F. ) <-> ( E. x ph -> F. ) )
4		dfnot 1416	. . 3 |- ( -. ph <-> ( ph -> F. ) )
5	4	albii 1519	. 2 |- ( A. x -. ph <-> A. x ( ph -> F. ) )
6		dfnot 1416	. 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 1396   F. wfal 1403   E.wex 1541

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ie2 1543

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-fal 1404

This theorem is referenced by:  nex  1549  dfexdc  1550  exalim  1551  ax-9  1580  alinexa  1652  nexd  1662  alexdc  1668  19.30dc  1676  19.33b2  1678  alexnim  1697  nnal  1698  hbn  1699  nf4dc  1718  nf4r  1719  mo2n  2108  notm0  3529  disjsn  3751  snprc  3754  dm0rn0  4973  reldm0  4974  dmsn0  5230  dmsn0el  5232  iotanul  5328  imadiflem  5435  imadif  5436  ltexprlemdisj  7921  recexprlemdisj  7945  fzo0  10504