Theorem exnal 1854

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1565  ∃wex 1806

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

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

This theorem is referenced by:  alexn  1872  nfnbi  1882  exanali  1886  19.35  1904  19.30  1908  nfeqf2  2415  nabbib  3069  r2exlem  3160  spc3gv  3572  vn0  4306  notzfaus  5332  dtruALT2  5339  dvdemo1  5342  dtruALT  5357  eunex  5359  reusv2lem2  5368  dtru  5416  brprcneu  6869  brprcneuALT  6870  dffv2  6974  zfcndpow  10597  hashfun  14470  nmo  32773  bnj1304  35148  bnj1253  35346  axregs  35471  onvf1odlem4  35485  axrepprim  36089  axunprim  36090  axregprim  36092  axinfprim  36093  axacprim  36094  dftr6  36138  brtxpsd  36279  elfuns  36300  dfrdg4  36338  bj-cbvaw  37148  relowlpssretop  37893  onsupmaxb  43853  clsk3nimkb  44653  expandexn  44886  vk15.4j  45124  vk15.4jVD  45509  alneu  47745