Theorem exnal 1619

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 1618	. 2 |- ( A. x ph <-> -. E. x -. ph )
2	1	con2bii 332	1 |- ( E. x -. ph <-> -. A. 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  ax-gen 1592  ax-4 1603

This theorem depends on definitions:  df-bi 185  df-ex 1588

This theorem is referenced by:  alexn  1632  exanali  1638  19.35  1655  19.30  1660  excom  1789  nfeqf2  2001  nabbi  2784  nabbiOLD  2785  spc3gv  3166  notzfaus  4574  dtru  4590  eunex  4592  reusv2lem2  4601  dtruALT  4631  dvdemo1  4634  dtruALT2  4643  brprcneu  5791  dffv2  5872  zfcndpow  8893  hashfun  12316  nmo  26020  axrepprim  27496  axunprim  27497  axregprim  27499  axinfprim  27500  axacprim  27501  dftr6  27703  brtxpsd  28068  elfuns  28089  dfrdg4  28124  alneu  30172  vk15.4j  31550  vk15.4jVD  31967  bnj1304  32130  bnj1253  32325  bj-dtru  32635  bj-eunex  32637  bj-dvdemo1  32640