Theorem exnal 1696

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

Assertion

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

Proof of Theorem exnal

Step	Hyp	Ref	Expression
1		alex 1695	. 2 |- ( A. x ph <-> -. E. x -. ph )
2	1	con2bii 334	1 |- ( E. x -. ph <-> -. A. x ph )

Syntax hints:   -. wn 3   <-> wb 188   A.wal 1436   E.wex 1660

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

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

This theorem is referenced by:  alexn  1710  exanali  1716  19.35  1733  19.30  1737  excomOLD  1901  nfeqf2  2097  nabbi  2759  nabbiOLD  2760  r2exlem  2949  spc3gv  3172  notzfaus  4597  dtru  4613  eunex  4615  reusv2lem2  4624  dtruALT  4651  dvdemo1  4654  dtruALT2  4663  brprcneu  5872  dffv2  5952  zfcndpow  9043  hashfun  12608  nmo  28113  bnj1304  29633  bnj1253  29828  axrepprim  30331  axunprim  30332  axregprim  30334  axinfprim  30335  axacprim  30336  dftr6  30391  brtxpsd  30660  elfuns  30681  dfrdg4  30717  bj-dtru  31376  bj-eunex  31378  bj-dvdemo1  31381  relowlpssretop  31725  vk15.4j  36787  vk15.4jVD  37216  alneu  38379