Theorem exnal 1825

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1535  ∃wex 1777

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

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

This theorem is referenced by:  alexn  1843  nfnbi  1853  exanali  1858  19.35  1876  19.30  1880  nfeqf2  2385  nabbib  3051  r2exlem  3149  spc3gv  3617  vn0  4368  notzfaus  5381  dtruALT2  5388  dvdemo1  5391  dtruALT  5406  eunex  5408  reusv2lem2  5417  dtru  5456  dtruOLD  5461  brprcneu  6910  brprcneuALT  6911  dffv2  7017  zfcndpow  10685  hashfun  14486  nmo  32518  bnj1304  34795  bnj1253  34993  axrepprim  35664  axunprim  35665  axregprim  35667  axinfprim  35668  axacprim  35669  dftr6  35713  brtxpsd  35858  elfuns  35879  dfrdg4  35915  relowlpssretop  37330  onsupmaxb  43200  clsk3nimkb  44002  expandexn  44258  vk15.4j  44499  vk15.4jVD  44885  alneu  47039