Theorem alnex 1598

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 1597	. 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 1377   E.wex 1596

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 1597

This theorem is referenced by:  nex  1610  alex  1627  2exnaln  1630  aleximi  1632  eximOLD  1634  19.38  1639  alinexa  1640  alexn  1641  nexdh  1651  19.35OLD  1665  19.43  1670  19.43OLD  1671  19.33b  1673  nf4  1911  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  moOLD  2327  mo2OLD  2336  2moOLDOLD  2384  mo2icl  3282  disjsn  4088  dm0rn0  5219  reldm0  5220  iotanul  5566  imadif  5663  dffv2  5941  kmlem4  8534  axpowndlem3  8976  axpowndlem3OLD  8977  axpownd  8979  hashgt0elex  12433  nmo  27157  wl-nfeqfb  29843  wl-sb8et  29854  wl-lem-nexmo  29869  n0el  30431  pm10.251  31070  pm10.57  31081  elnev  31150  usgedgnlp  32104  alimp-no-surprise  32494  bnj1143  33145  bj-nf3  33497  bj-nexdh  33519  bj-hbntbi  33557