Theorem alnex 1431

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 1433 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 1294	. . . 4 |- -. F.
2	1	pm2.21i 608	. . 3 |- ( F. -> A. x F. )
3	2	19.23h 1430	. 2 |- ( A. x ( ph -> F. ) <-> ( E. x ph -> F. ) )
4		dfnot 1305	. . 3 |- ( -. ph <-> ( ph -> F. ) )
5	4	albii 1402	. 2 |- ( A. x -. ph <-> A. x ( ph -> F. ) )
6		dfnot 1305	. 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 1285   F. wfal 1292   E.wex 1424

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 1379  ax-gen 1381  ax-ie2 1426

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-fal 1293

This theorem is referenced by:  nex  1432  dfexdc  1433  exalim  1434  ax-9  1467  alinexa  1537  nexd  1547  alexdc  1553  19.30dc  1561  19.33b2  1563  alexnim  1582  ax6blem  1583  nf4dc  1603  nf4r  1604  mo2n  1973  notm0  3292  disjsn  3487  snprc  3490  dm0rn0  4621  reldm0  4622  dmsn0  4864  dmsn0el  4866  iotanul  4961  imadiflem  5058  imadif  5059  ltexprlemdisj  7109  recexprlemdisj  7133  fzo0  9507