Theorem exnal 1669

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

Syntax hints:   -. wn 3   <-> wb 184   A.wal 1403   E.wex 1633

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

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

This theorem is referenced by:  alexn  1685  exanali  1691  19.35  1708  19.30  1713  excom  1873  nfeqf2  2067  nabbi  2737  nabbiOLD  2738  r2exlem  2927  spc3gv  3149  notzfaus  4569  dtru  4585  eunex  4587  reusv2lem2  4596  dtruALT  4623  dvdemo1  4626  dtruALT2  4635  brprcneu  5842  dffv2  5922  zfcndpow  9024  hashfun  12544  nmo  27799  bnj1304  29205  bnj1253  29400  axrepprim  29903  axunprim  29904  axregprim  29906  axinfprim  29907  axacprim  29908  dftr6  29963  brtxpsd  30232  elfuns  30253  dfrdg4  30289  bj-dtru  30947  bj-eunex  30949  bj-dvdemo1  30952  relowlpssretop  31281  vk15.4j  36315  vk15.4jVD  36745  alneu  37574