Theorem exnal 1826

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 1825. 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 1825	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2	1	con2bii 360	1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1534  ∃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 209  df-ex 1780

This theorem is referenced by:  alexn  1844  exanali  1858  19.35  1877  19.30  1881  nfeqf2  2394  nabbi  3124  r2exlem  3305  spc3gv  3608  notzfaus  5265  notzfausOLD  5266  dtru  5274  dvdemo1  5277  dtruALT  5292  eunex  5294  reusv2lem2  5303  dtruALT2  5339  brprcneu  6665  dffv2  6759  zfcndpow  10041  hashfun  13801  nmo  30257  bnj1304  32095  bnj1253  32293  axrepprim  32932  axunprim  32933  axregprim  32935  axinfprim  32936  axacprim  32937  dftr6  32990  brtxpsd  33359  elfuns  33380  dfrdg4  33416  bj-dtru  34143  relowlpssretop  34649  sn-dtru  39117  clsk3nimkb  40396  expandexn  40631  vk15.4j  40868  vk15.4jVD  41254  alneu  43330