Theorem exnal 1859

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

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

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

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

This theorem is used by:  alexn  1877  nfnbi  1887  exanali  1891  19.35  1909  19.30  1913  nfeqf2  2406  nabbib  3060  r2exlem  3151  spc3gv  3558  vn0OLD  4291  notsep  5324  dtruALT2  5331  dvdemo1  5334  dtruALT  5349  eunex  5351  reusv2lem2  5360  dtru  5404  brprcneu  6878  brprcneuALT  6879  dffv2  6983  zfcndpow  10706  hashfun  14587  degenmgm2nfun  19146  nmo  33135  bnj1304  35497  bnj1253  35695  axregs  35865  onvf1odlem4  35955  axrepprim  36561  axunprim  36562  axregprim  36564  axinfprim  36565  axacprim  36566  dftr6  36610  brtxpsd  36750  elfuns  36771  dfrdg4  36809  bj-cbvaw  37634  relowlpssretop  38394  onsupmaxb  44348  clsk3nimkb  45147  expandexn  45380  vk15.4j  45618  vk15.4jVD  46003  alneu  48301