Theorem exnal 1834

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

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wal 1545  ∃wex 1786

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

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  alexn  1852  nfnbi  1862  exanali  1866  19.35  1884  19.30  1888  nfeqf2  2385  nabbib  3037  r2exlem  3128  spc3gv  3542  vn0  4273  notzfaus  5292  dtruALT2  5299  dvdemo1  5302  dtruALT  5317  eunex  5319  reusv2lem2  5328  dtru  5376  brprcneu  6817  brprcneuALT  6818  dffv2  6922  zfcndpow  10530  hashfun  14390  nmo  32577  bnj1304  35001  bnj1253  35199  axregs  35320  onvf1odlem4  35334  axrepprim  35930  axunprim  35931  axregprim  35933  axinfprim  35934  axacprim  35935  dftr6  35979  brtxpsd  36120  elfuns  36141  dfrdg4  36179  bj-cbvaw  36981  relowlpssretop  37726  onsupmaxb  43684  clsk3nimkb  44484  expandexn  44733  vk15.4j  44972  vk15.4jVD  45357  alneu  47587