Theorem exnal 1860

Description: Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1814. See also the dual pair df-ex 1813 / alex 1859. 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 1859	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2	1	con2bii 360	1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  alexn  1878  nfnbi  1888  exanali  1892  19.35  1910  19.30  1914  nfeqf2  2407  nabbib  3061  r2exlem  3152  spc3gv  3559  vn0OLD  4292  notsep  5325  dtruALT2  5332  dvdemo1  5335  dtruALT  5350  eunex  5352  reusv2lem2  5361  dtru  5405  brprcneu  6873  brprcneuALT  6874  dffv2  6978  zfcndpow  10694  hashfun  14575  degenmgm2nfun  19132  nmo  33079  bnj1304  35442  bnj1253  35640  axregs  35790  onvf1odlem4  35868  axrepprim  36446  axunprim  36447  axregprim  36449  axinfprim  36450  axacprim  36451  dftr6  36495  brtxpsd  36636  elfuns  36657  dfrdg4  36695  bj-cbvaw  37520  relowlpssretop  38267  onsupmaxb  44225  clsk3nimkb  45025  expandexn  45258  vk15.4j  45496  vk15.4jVD  45881  alneu  48163