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  31761  bnj1304  33861  bnj1253  34059  axrepprim  34702  axunprim  34703  axregprim  34705  axinfprim  34706  axacprim  34707  dftr6  34752  brtxpsd  34897  elfuns  34918  dfrdg4  34954  relowlpssretop  36293  onsupmaxb  42036  clsk3nimkb  42839  expandexn  43096  vk15.4j  43337  vk15.4jVD  43723  alneu  45880