Theorem exnal 1828

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1539  ∃wex 1780

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

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

This theorem is referenced by:  alexn  1846  nfnbi  1856  exanali  1860  19.35  1878  19.30  1882  nfeqf2  2379  nabbib  3032  r2exlem  3122  spc3gv  3555  vn0  4294  notzfaus  5305  dtruALT2  5312  dvdemo1  5315  dtruALT  5330  eunex  5332  reusv2lem2  5341  dtru  5383  brprcneu  6821  brprcneuALT  6822  dffv2  6926  zfcndpow  10518  hashfun  14351  nmo  32490  bnj1304  34903  bnj1253  35101  axregs  35217  onvf1odlem4  35222  axrepprim  35818  axunprim  35819  axregprim  35821  axinfprim  35822  axacprim  35823  dftr6  35867  brtxpsd  36008  elfuns  36029  dfrdg4  36067  relowlpssretop  37481  onsupmaxb  43396  clsk3nimkb  44197  expandexn  44446  vk15.4j  44685  vk15.4jVD  45070  alneu  47286