Theorem exnal 1830

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537  ∃wex 1783

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

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

This theorem is referenced by:  alexn  1848  nfnbi  1858  exanali  1863  19.35  1881  19.30  1885  nfeqf2  2377  nabbi  3046  r2exlem  3230  spc3gv  3533  vn0  4269  notzfaus  5280  dtru  5288  dvdemo1  5291  dtruALT  5306  eunex  5308  reusv2lem2  5317  dtruALT2  5353  brprcneu  6747  fvprc  6748  dffv2  6845  zfcndpow  10303  hashfun  14080  nmo  30739  bnj1304  32699  bnj1253  32897  axrepprim  33543  axunprim  33544  axregprim  33546  axinfprim  33547  axacprim  33548  dftr6  33624  brtxpsd  34123  elfuns  34144  dfrdg4  34180  bj-dtru  34926  relowlpssretop  35462  sn-dtru  40116  clsk3nimkb  41539  expandexn  41796  vk15.4j  42037  vk15.4jVD  42423  alneu  44503