Theorem exnal 1829

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537  ∃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  1847  nfnbi  1857  exanali  1862  19.35  1880  19.30  1884  nfeqf2  2377  nabbi  3047  r2exlem  3231  spc3gv  3543  vn0  4272  notzfaus  5285  dtruALT2  5293  dvdemo1  5296  dtruALT  5311  eunex  5313  reusv2lem2  5322  dtru  5359  brprcneu  6764  brprcneuALT  6765  dffv2  6863  zfcndpow  10372  hashfun  14152  nmo  30838  bnj1304  32799  bnj1253  32997  axrepprim  33643  axunprim  33644  axregprim  33646  axinfprim  33647  axacprim  33648  dftr6  33718  brtxpsd  34196  elfuns  34217  dfrdg4  34253  bj-dtru  34999  relowlpssretop  35535  sn-dtru  40188  clsk3nimkb  41650  expandexn  41907  vk15.4j  42148  vk15.4jVD  42534  alneu  44616