Theorem exnal 1827

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538  ∃wex 1779

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

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

This theorem is referenced by:  alexn  1845  nfnbi  1855  exanali  1859  19.35  1877  19.30  1881  nfeqf2  2381  nabbib  3035  r2exlem  3129  spc3gv  3583  vn0  4320  notzfaus  5333  dtruALT2  5340  dvdemo1  5343  dtruALT  5358  eunex  5360  reusv2lem2  5369  dtru  5411  dtruOLD  5416  brprcneu  6865  brprcneuALT  6866  dffv2  6973  zfcndpow  10628  hashfun  14453  nmo  32417  bnj1304  34796  bnj1253  34994  axrepprim  35665  axunprim  35666  axregprim  35668  axinfprim  35669  axacprim  35670  dftr6  35714  brtxpsd  35858  elfuns  35879  dfrdg4  35915  relowlpssretop  37328  onsupmaxb  43210  clsk3nimkb  44011  expandexn  44261  vk15.4j  44501  vk15.4jVD  44886  alneu  47101