Theorem alnex 1706

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

Syntax hints:  ¬ wn 3   ↔ wb 196  ∀wal 1481  ∃wex 1704

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 197  df-ex 1705

This theorem is referenced by:  nf3  1712  nex  1731  alex  1753  2exnaln  1756  aleximi  1759  19.38  1766  alinexa  1770  alexn  1771  nexdh  1792  19.43  1810  19.43OLD  1811  19.33b  1813  nexdvOLD  1865  cbvexdva  2283  mo2v  2477  ralnex  2992  mo2icl  3385  n0el  3940  falseral0  4081  disjsn  4246  dm0rn0  5342  reldm0  5343  iotanul  5866  imadif  5973  dffv2  6271  kmlem4  8975  axpowndlem3  9421  axpownd  9423  hashgt0elex  13189  nmo  29325  bnj1143  30861  unbdqndv1  32499  bj-nexdh  32606  bj-modal5e  32636  axc11n11r  32673  bj-hbntbi  32695  bj-modal4e  32705  wl-nfeqfb  33323  wl-sb8et  33334  wl-lem-nexmo  33349  pm10.251  38559  pm10.57  38570  elnev  38639  spr0nelg  41726  zrninitoringc  42071  alimp-no-surprise  42527