Theorem exnal 1857

Description: Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1811. See also the dual pair df-ex 1810 / alex 1856. Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)

Assertion

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

Proof of Theorem exnal

Step	Hyp	Ref	Expression
1		alex 1856	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2	1	con2bii 360	1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1568  ∃wex 1809

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

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  alexn  1875  nfnbi  1885  exanali  1889  19.35  1907  19.30  1911  nfeqf2  2409  nabbib  3063  r2exlem  3154  spc3gv  3563  vn0OLD  4299  notsep  5334  dtruALT2  5341  dvdemo1  5344  dtruALT  5359  eunex  5361  reusv2lem2  5370  dtru  5418  brprcneu  6871  brprcneuALT  6872  dffv2  6976  zfcndpow  10596  hashfun  14470  nmo  32836  bnj1304  35207  bnj1253  35405  axregs  35552  onvf1odlem4  35590  axrepprim  36194  axunprim  36195  axregprim  36197  axinfprim  36198  axacprim  36199  dftr6  36243  brtxpsd  36384  elfuns  36405  dfrdg4  36443  bj-cbvaw  37263  relowlpssretop  38010  onsupmaxb  43966  clsk3nimkb  44766  expandexn  44999  vk15.4j  45237  vk15.4jVD  45622  alneu  47861