Theorem alnex 1388

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 1390 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 1250	. . . 4 |- -. F.
2	1	pm2.21i 575	. . 3 |- ( F. -> A. x F. )
3	2	19.23h 1387	. 2 |- ( A. x ( ph -> F. ) <-> ( E. x ph -> F. ) )
4		dfnot 1262	. . 3 |- ( -. ph <-> ( ph -> F. ) )
5	4	albii 1359	. 2 |- ( A. x -. ph <-> A. x ( ph -> F. ) )
6		dfnot 1262	. 2 |- ( -. E. x ph <-> ( E. x ph -> F. ) )
7	3, 5, 6	3bitr4i 201	1 |- ( A. x -. ph <-> -. E. x ph )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 98   A.wal 1241   F. wfal 1248   E.wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-5 1336  ax-gen 1338  ax-ie2 1383

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-fal 1249

This theorem is referenced by:  nex  1389  dfexdc  1390  exalim  1391  ax-9  1424  alinexa  1494  nexd  1504  alexdc  1510  19.30dc  1518  19.33b2  1520  alexnim  1539  ax6blem  1540  nf4dc  1560  nf4r  1561  mo2n  1928  disjsn  3432  snprc  3435  dm0rn0  4552  reldm0  4553  dmsn0  4788  dmsn0el  4790  iotanul  4882  imadiflem  4978  imadif  4979  ltexprlemdisj  6704  recexprlemdisj  6728  fzo0  9024