Theorem exnal 1828

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1539  ∃wex 1780

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

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

This theorem is referenced by:  alexn  1846  nfnbi  1856  exanali  1860  19.35  1878  19.30  1882  nfeqf2  2381  nabbib  3035  r2exlem  3125  spc3gv  3558  vn0  4297  notzfaus  5308  dtruALT2  5315  dvdemo1  5318  dtruALT  5333  eunex  5335  reusv2lem2  5344  dtru  5386  brprcneu  6824  brprcneuALT  6825  dffv2  6929  zfcndpow  10527  hashfun  14360  nmo  32564  bnj1304  34975  bnj1253  35173  axregs  35295  onvf1odlem4  35300  axrepprim  35896  axunprim  35897  axregprim  35899  axinfprim  35900  axacprim  35901  dftr6  35945  brtxpsd  36086  elfuns  36107  dfrdg4  36145  relowlpssretop  37569  onsupmaxb  43481  clsk3nimkb  44281  expandexn  44530  vk15.4j  44769  vk15.4jVD  45154  alneu  47370