Theorem alnex 1486

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 1488 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 1349	. . . 4 |- -. F.
2	1	pm2.21i 636	. . 3 |- ( F. -> A. x F. )
3	2	19.23h 1485	. 2 |- ( A. x ( ph -> F. ) <-> ( E. x ph -> F. ) )
4		dfnot 1360	. . 3 |- ( -. ph <-> ( ph -> F. ) )
5	4	albii 1457	. 2 |- ( A. x -. ph <-> A. x ( ph -> F. ) )
6		dfnot 1360	. 2 |- ( -. E. x ph <-> ( E. x ph -> F. ) )
7	3, 5, 6	3bitr4i 211	1 |- ( A. x -. ph <-> -. E. x ph )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104   A.wal 1340   F. wfal 1347   E.wex 1479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1434  ax-gen 1436  ax-ie2 1481

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-fal 1348

This theorem is referenced by:  nex  1487  dfexdc  1488  exalim  1489  ax-9  1518  alinexa  1590  nexd  1600  alexdc  1606  19.30dc  1614  19.33b2  1616  alexnim  1635  nnal  1636  ax6blem  1637  nf4dc  1657  nf4r  1658  mo2n  2041  notm0  3424  disjsn  3632  snprc  3635  dm0rn0  4815  reldm0  4816  dmsn0  5065  dmsn0el  5067  iotanul  5162  imadiflem  5261  imadif  5262  ltexprlemdisj  7538  recexprlemdisj  7562  fzo0  10093