Theorem exnal 1628

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

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

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

This theorem is referenced by:  alexn  1641  exanali  1647  19.35  1664  19.30  1669  excom  1798  nfeqf2  2014  nabbi  2800  nabbiOLD  2801  r2exlem  2982  spc3gv  3203  notzfaus  4622  dtru  4638  eunex  4640  reusv2lem2  4649  dtruALT  4679  dvdemo1  4682  dtruALT2  4691  brprcneu  5857  dffv2  5938  zfcndpow  8990  hashfun  12457  nmo  27060  axrepprim  28549  axunprim  28550  axregprim  28552  axinfprim  28553  axacprim  28554  dftr6  28756  brtxpsd  29121  elfuns  29142  dfrdg4  29177  alneu  31673  vk15.4j  32377  vk15.4jVD  32794  bnj1304  32957  bnj1253  33152  bj-dtru  33464  bj-eunex  33466  bj-dvdemo1  33469