Theorem alnex 1545

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 1547 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 1402	. . . 4 |- -. F.
2	1	pm2.21i 649	. . 3 |- ( F. -> A. x F. )
3	2	19.23h 1544	. 2 |- ( A. x ( ph -> F. ) <-> ( E. x ph -> F. ) )
4		dfnot 1413	. . 3 |- ( -. ph <-> ( ph -> F. ) )
5	4	albii 1516	. 2 |- ( A. x -. ph <-> A. x ( ph -> F. ) )
6		dfnot 1413	. 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 1393   F. wfal 1400   E.wex 1538

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-ie2 1540

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

This theorem is referenced by:  nex  1546  dfexdc  1547  exalim  1548  ax-9  1577  alinexa  1649  nexd  1659  alexdc  1665  19.30dc  1673  19.33b2  1675  alexnim  1694  nnal  1695  ax6blem  1696  nf4dc  1716  nf4r  1717  mo2n  2105  notm0  3512  disjsn  3728  snprc  3731  dm0rn0  4940  reldm0  4941  dmsn0  5196  dmsn0el  5198  iotanul  5294  imadiflem  5400  imadif  5401  ltexprlemdisj  7793  recexprlemdisj  7817  fzo0  10366