Theorem alnex 1661

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 1660	. 2 |- ( E. x ph <-> -. A. x -. ph )
2	1	con2bii 333	1 |- ( A. x -. ph <-> -. E. x ph )

Syntax hints:   -. wn 3   <-> wb 187   A.wal 1435   E.wex 1659

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 188  df-ex 1660

This theorem is referenced by:  nex  1674  alex  1694  2exnaln  1697  aleximi  1700  19.38  1707  alinexa  1708  alexn  1709  nexdh  1719  19.43  1737  19.43OLD  1738  19.33b  1740  nexdv  1771  nf4  2017  mo2v  2270  mo2vOLD  2271  mo2icl  3247  disjsn  4054  dm0rn0  5062  reldm0  5063  iotanul  5571  imadif  5667  dffv2  5945  kmlem4  8572  axpowndlem3  9013  axpownd  9015  hashgt0elex  12564  nmo  27982  bnj1143  29416  bj-nf3  31002  bj-nexdh  31019  bj-hbntbi  31064  wl-nfeqfb  31603  wl-sb8et  31614  wl-lem-nexmo  31629  n0el  32168  pm10.251  36379  pm10.57  36390  elnev  36459  zrninitoringc  38873  alimp-no-surprise  39323