Theorem alnex 1385

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 1387 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.xph)

Proof of Theorem alnex

Step	Hyp	Ref	Expression
1		fal 1249	. . . 4 |- -. F.
2	1	pm2.21i 574	. . 3 |- ( F. -> A.x F. )
3	2	19.23h 1384	. 2 |- (A.x(ph -> F. ) <-> (E.xph -> F. ))
4		dfnot 1261	. . 3 |- (-. ph <-> (ph -> F. ))
5	4	albii 1356	. 2 |- (A.x -. ph <-> A.x(ph -> F. ))
6		dfnot 1261	. 2 |- (-. E.xph <-> (E.xph -> F. ))
7	3, 5, 6	3bitr4i 201	1 |- (A.x -. ph <-> -. E.xph)

Syntax hints:  -. wn 3   -> wi 4   <-> wb 98  A.wal 1240   F. wfal 1247  E.wex 1378

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 1333  ax-gen 1335  ax-ie2 1380

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-fal 1248

This theorem is referenced by:  nex  1386  dfexdc  1387  exalim  1388  ax-9  1421  alinexa  1491  nexd  1501  alexdc  1507  19.30dc  1515  19.33b2  1517  alexnim  1536  ax6blem  1537  nf4dc  1557  nf4r  1558  mo2n  1925  disjsn  3423  snprc  3426  dm0rn0  4495  reldm0  4496  dmsn0  4731  dmsn0el  4733  iotanul  4825  imadiflem  4921  imadif  4922  ltexprlemdisj  6578  recexprlemdisj  6600  fzo0  8754