Theorem alnex 1697

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 1696	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
2	1	con2bii 346	1 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 195  ∀wal 1473  ∃wex 1695

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 196  df-ex 1696

This theorem is referenced by:  nf3  1703  nex  1722  alex  1743  2exnaln  1746  aleximi  1749  19.38  1757  alinexa  1759  alexn  1760  nexdh  1779  19.43  1799  19.43OLD  1800  19.33b  1802  nexdvOLD  1852  cbvexdva  2271  mo2v  2465  ralnex  2975  mo2icl  3352  disjsn  4192  dm0rn0  5263  reldm0  5264  iotanul  5783  imadif  5887  dffv2  6181  kmlem4  8858  axpowndlem3  9300  axpownd  9302  hashgt0elex  13050  nmo  28709  bnj1143  30115  unbdqndv1  31669  bj-nf3  31767  bj-nexdh  31790  bj-modal5e  31825  axc11n11r  31860  bj-hbntbi  31882  bj-modal4e  31892  wl-nfeqfb  32502  wl-sb8et  32513  wl-lem-nexmo  32528  n0el  33164  pm10.251  37581  pm10.57  37592  elnev  37661  falseral0  40308  zrninitoringc  41863  alimp-no-surprise  42336