Theorem exnal 1574

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

Assertion

Ref	Expression
exnal	⊢ (∃x ¬ φ ↔ ¬ ∀xφ)

Proof of Theorem exnal

Step	Hyp	Ref	Expression
1		alex 1572	. 2 ⊢ (∀xφ ↔ ¬ ∃x ¬ φ)
2	1	con2bii 322	1 ⊢ (∃x ¬ φ ↔ ¬ ∀xφ)

Syntax hints:  ¬ wn 3   ↔ wb 176  ∀wal 1540  ∃wex 1541

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

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  alexn  1579  exanali  1585  19.30  1604  excom  1741  ax12olem5  1931  ax10lem2  1937  equsex  1962  spc3gv  2945  necompl  3545  opkelimagekg  4272  dfpw2  4328  dfaddc2  4382  nnsucelrlem1  4425  eqpw1relk  4480  eqtfinrelk  4487  setconslem2  4733  setconslem3  4734  setconslem7  4738  dfswap2  4742  nfunv  5139  brimage  5794  releqel  5808  releqmpt2  5810  ovcelem1  6172  tcfnex  6245  nchoicelem10  6299  fnfreclem1  6318