Theorem exnal 1830

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1540  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  alexn  1848  nfnbi  1858  exanali  1863  19.35  1881  19.30  1885  nfeqf2  2377  nabbib  3046  r2exlem  3144  spc3gv  3595  vn0  4339  notzfaus  5362  dtruALT2  5369  dvdemo1  5372  dtruALT  5387  eunex  5389  reusv2lem2  5398  dtru  5437  dtruOLD  5442  brprcneu  6882  brprcneuALT  6883  dffv2  6987  zfcndpow  10611  hashfun  14397  nmo  31730  bnj1304  33830  bnj1253  34028  axrepprim  34671  axunprim  34672  axregprim  34674  axinfprim  34675  axacprim  34676  dftr6  34721  brtxpsd  34866  elfuns  34887  dfrdg4  34923  relowlpssretop  36245  onsupmaxb  41988  clsk3nimkb  42791  expandexn  43048  vk15.4j  43289  vk15.4jVD  43675  alneu  45832