Theorem exnal 1580

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

Assertion

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

Proof of Theorem exnal

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

Syntax hints:   -. wn 3   <-> wb 177   A.wal 1546   E.wex 1547

This theorem is referenced by:  alexn  1586  exanali  1592  19.30  1611  excom  1752  equsexOLD  1970  ax12olem3  1974  ax12olem5OLD  1981  ax10lem2OLD  1992  spc3gv  3001  notzfaus  4334  dtru  4350  eunex  4352  dtruALT  4356  dvdemo1  4359  dtruALT2  4368  reusv2lem2  4684  brprcneu  5680  dffv2  5755  zfcndpow  8447  hashfun  11655  nmo  23926  axrepprim  25104  axunprim  25105  axregprim  25107  axinfprim  25108  axacprim  25109  dftr6  25321  brtxpsd  25648  dfrdg4  25703  alneu  27846  vk15.4j  28323  vk15.4jVD  28735  bnj1304  28897  bnj1253  29092  equsexNEW7  29196

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563

This theorem depends on definitions:  df-bi 178  df-ex 1548