Theorem alnex 1694

Description: Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)

Assertion

Ref	Expression
alnex	⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Proof of Theorem alnex

Step	Hyp	Ref	Expression
1		df-ex 1693	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
2	1	con2bii 341	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 191  ∀wal 1466  ∃wex 1692

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

This theorem depends on definitions:  df-bi 192  df-ex 1693

This theorem is referenced by:  nex  1707  alex  1729  2exnaln  1732  aleximi  1735  19.38  1743  alinexa  1744  alexn  1745  nexdh  1756  19.43  1776  19.43OLD  1777  19.33b  1779  nexdv  1813  nf4  2095  mo2v  2360  mo2icl  3241  disjsn  4060  dm0rn0  5100  reldm0  5101  iotanul  5612  imadif  5713  dffv2  6005  kmlem4  8668  axpowndlem3  9109  axpownd  9111  hashgt0elex  12696  nmo  28282  bnj1143  29754  unbdqndv1  31306  bj-nf3  31377  bj-nexdh  31396  bj-modal5e  31431  bj-hbntbi  31483  bj-modal4e  31493  wl-nfeqfb  32101  wl-sb8et  32112  wl-lem-nexmo  32127  n0el  32666  pm10.251  37066  pm10.57  37077  elnev  37146  falseral0  39508  zrninitoringc  41263  alimp-no-surprise  41707