Theorem alnex 1746

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

Syntax hints:  ¬ wn 3   ↔ wb 196  ∀wal 1521  ∃wex 1744

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 1745

This theorem is referenced by:  nf3  1752  nex  1771  alex  1793  2exnaln  1796  aleximi  1799  19.38  1806  alinexa  1810  alexn  1811  nexdh  1832  19.43  1850  19.43OLD  1851  19.33b  1853  nexdvOLD  1905  cbvexdva  2319  mo2v  2505  ralnex  3021  mo2icl  3418  n0el  3973  falseral0  4114  disjsn  4278  dm0rn0  5374  reldm0  5375  iotanul  5904  imadif  6011  dffv2  6310  kmlem4  9013  axpowndlem3  9459  axpownd  9461  hashgt0elex  13227  iswspthsnon  26806  nmo  29453  bnj1143  30987  unbdqndv1  32624  bj-nexdh  32731  bj-modal5e  32761  axc11n11r  32798  bj-hbntbi  32820  bj-modal4e  32830  wl-nfeqfb  33453  wl-sb8et  33464  wl-lem-nexmo  33479  pm10.251  38876  pm10.57  38887  elnev  38956  spr0nelg  42051  zrninitoringc  42396  alimp-no-surprise  42855