Theorem alnex 1429

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 1431 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 1292	. . . 4 |- -. F.
2	1	pm2.21i 608	. . 3 |- ( F. -> A. x F. )
3	2	19.23h 1428	. 2 |- ( A. x ( ph -> F. ) <-> ( E. x ph -> F. ) )
4		dfnot 1303	. . 3 |- ( -. ph <-> ( ph -> F. ) )
5	4	albii 1400	. 2 |- ( A. x -. ph <-> A. x ( ph -> F. ) )
6		dfnot 1303	. 2 |- ( -. E. x ph <-> ( E. x ph -> F. ) )
7	3, 5, 6	3bitr4i 210	1 |- ( A. x -. ph <-> -. E. x ph )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 103   A.wal 1283   F. wfal 1290   E.wex 1422

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-5 1377  ax-gen 1379  ax-ie2 1424

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-fal 1291

This theorem is referenced by:  nex  1430  dfexdc  1431  exalim  1432  ax-9  1465  alinexa  1535  nexd  1545  alexdc  1551  19.30dc  1559  19.33b2  1561  alexnim  1580  ax6blem  1581  nf4dc  1601  nf4r  1602  mo2n  1971  disjsn  3472  snprc  3475  dm0rn0  4600  reldm0  4601  dmsn0  4838  dmsn0el  4840  iotanul  4932  imadiflem  5029  imadif  5030  ltexprlemdisj  6928  recexprlemdisj  6952  fzo0  9324