Theorem exnal 1829

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1540  ∃wex 1781

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

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  alexn  1847  nfnbi  1857  exanali  1861  19.35  1879  19.30  1883  nfeqf2  2382  nabbib  3036  r2exlem  3127  spc3gv  3547  vn0  4286  notzfaus  5300  dtruALT2  5307  dvdemo1  5310  dtruALT  5325  eunex  5327  reusv2lem2  5336  dtru  5384  brprcneu  6824  brprcneuALT  6825  dffv2  6929  zfcndpow  10530  hashfun  14390  nmo  32574  bnj1304  34977  bnj1253  35175  axregs  35299  onvf1odlem4  35304  axrepprim  35900  axunprim  35901  axregprim  35903  axinfprim  35904  axacprim  35905  dftr6  35949  brtxpsd  36090  elfuns  36111  dfrdg4  36149  bj-cbvaw  36951  relowlpssretop  37694  onsupmaxb  43685  clsk3nimkb  44485  expandexn  44734  vk15.4j  44973  vk15.4jVD  45358  alneu  47584