Theorem alnex 1703

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

Syntax hints:  ¬ wn 3   ↔ wb 196  ∀wal 1478  ∃wex 1701

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 1702

This theorem is referenced by:  nf3  1709  nex  1728  alex  1750  2exnaln  1753  aleximi  1756  19.38  1763  alinexa  1767  alexn  1768  nexdh  1790  19.43  1810  19.43OLD  1811  19.33b  1813  nexdvOLD  1867  cbvexdva  2287  mo2v  2481  ralnex  2991  mo2icl  3372  falseral0  4058  disjsn  4221  dm0rn0  5306  reldm0  5307  iotanul  5828  imadif  5933  dffv2  6229  kmlem4  8920  axpowndlem3  9366  axpownd  9368  hashgt0elex  13126  nmo  29165  bnj1143  30561  unbdqndv1  32114  bj-nexdh  32221  bj-modal5e  32251  axc11n11r  32288  bj-hbntbi  32310  bj-modal4e  32320  wl-nfeqfb  32931  wl-sb8et  32942  wl-lem-nexmo  32957  n0el  33593  pm10.251  38008  pm10.57  38019  elnev  38088  spr0nelg  40983  zrninitoringc  41313  alimp-no-surprise  41785