Theorem exnal 1829

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1540  ∃wex 1781

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

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

This theorem is referenced by:  alexn  1847  nfnbi  1857  exanali  1861  19.35  1879  19.30  1883  nfeqf2  2382  nabbib  3036  r2exlem  3127  spc3gv  3560  vn0  4299  notzfaus  5310  dtruALT2  5317  dvdemo1  5320  dtruALT  5335  eunex  5337  reusv2lem2  5346  dtru  5393  brprcneu  6832  brprcneuALT  6833  dffv2  6937  zfcndpow  10539  hashfun  14372  nmo  32575  bnj1304  34994  bnj1253  35192  axregs  35314  onvf1odlem4  35319  axrepprim  35915  axunprim  35916  axregprim  35918  axinfprim  35919  axacprim  35920  dftr6  35964  brtxpsd  36105  elfuns  36126  dfrdg4  36164  bj-cbvaw  36881  relowlpssretop  37616  onsupmaxb  43593  clsk3nimkb  44393  expandexn  44642  vk15.4j  44881  vk15.4jVD  45266  alneu  47481