Theorem alnex 1589

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

Syntax hints:   -. wn 3   <-> wb 184   A.wal 1368   E.wex 1587

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 185  df-ex 1588

This theorem is referenced by:  nex  1601  alex  1618  2exnaln  1621  aleximi  1623  eximOLD  1625  19.38  1630  alinexa  1631  alexn  1632  nexdh  1642  19.35OLD  1656  19.43  1661  19.43OLD  1662  19.33b  1664  nf4  1902  mo2v  2269  mo2vOLD  2270  mo2vOLDOLD  2271  moOLD  2314  mo2OLD  2323  2moOLDOLD  2371  mo2icl  3245  disjsn  4047  dm0rn0  5167  reldm0  5168  iotanul  5507  imadif  5604  dffv2  5876  kmlem4  8436  axpowndlem3  8878  axpowndlem3OLD  8879  axpownd  8881  hashgt0elex  12280  nmo  26041  wl-nfeqfb  28534  wl-sb8et  28545  wl-lem-nexmo  28560  n0el  29172  pm10.251  29780  pm10.57  29791  elnev  29860  alimp-no-surprise  31485  bnj1143  32136  bj-nf3  32486  bj-nexdh  32508  bj-hbntbi  32546