Theorem alnex 716

Description: Theorem 19.7 of [Margaris] p. 89.

Assertion

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

Proof of Theorem alnex

Step	Hyp	Ref	Expression
1		df-ex 679	. 2 ⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
2	1	bicon2i 194	1 ⊢ (∀x ¬ φ ↔ ¬ ∃xφ)

Syntax hints:  ¬ wn 1   ↔ wb 127  ∀wal 672  ∃wex 678

This theorem is referenced by:  alex 717  alinexa 724  exanali 725  alexn 726  19.29 752  19.43 767  19.33b 771  19.41 774  nex 779  nexd 780  mo 1020  mo2 1026  mo2icl 1434  dm0rn0 2549  reldm0 2550  imadif 2714  fn0 2739  fvopabn 2873  kmlem4 3583  axpowndlem3 3745  axpownd 3747

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-ex 679

metamath.org