Theorem alnex 1664

Description: Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)

Assertion

Ref	Expression
alnex	|- ( A. x -. ph <-> -. E. x ph )

Proof of Theorem alnex

Step	Hyp	Ref	Expression
1		df-ex 1663	. 2 |- ( E. x ph <-> -. A. x -. ph )
2	1	con2bii 334	1 |- ( A. x -. ph <-> -. E. x ph )

Syntax hints:   -. wn 3   <-> wb 188   A.wal 1441   E.wex 1662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 189  df-ex 1663

This theorem is referenced by:  nex  1677  alex  1697  2exnaln  1700  aleximi  1703  19.38  1711  alinexa  1712  alexn  1713  nexdh  1724  19.43  1744  19.43OLD  1745  19.33b  1747  nexdv  1781  nf4  2042  mo2v  2305  mo2icl  3216  disjsn  4031  dm0rn0  5050  reldm0  5051  iotanul  5560  imadif  5656  dffv2  5936  kmlem4  8580  axpowndlem3  9021  axpownd  9023  hashgt0elex  12575  nmo  28114  bnj1143  29595  bj-nf3  31186  bj-nexdh  31207  bj-modal5e  31242  bj-hbntbi  31291  bj-modal4e  31301  wl-nfeqfb  31863  wl-sb8et  31874  wl-lem-nexmo  31889  n0el  32427  pm10.251  36703  pm10.57  36714  elnev  36783  falseral0  38980  zrninitoringc  40060  alimp-no-surprise  40507