Theorem alex 1572

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

Assertion

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

Proof of Theorem alex

Step	Hyp	Ref	Expression
1		notnot 282	. . 3 ⊢ (φ ↔ ¬ ¬ φ)
2	1	albii 1566	. 2 ⊢ (∀xφ ↔ ∀x ¬ ¬ φ)
3		alnex 1543	. 2 ⊢ (∀x ¬ ¬ φ ↔ ¬ ∃x ¬ φ)
4	2, 3	bitri 240	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:  2nalexn  1573  exnal  1574  19.3v  1665  hba1  1786  exists2  2294  nnsucelrlem1  4425  ltfinex  4465  eqpwrelk  4479  ncfinlowerlem1  4483  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  dfop2lem1  4574  funsex  5829  qsexg  5983