Theorem exnal 1833

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1540  ∃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 210  df-ex 1787

This theorem is referenced by:  alexn  1851  nfnbi  1861  exanali  1866  19.35  1884  19.30  1888  nfeqf2  2377  nabbi  3036  r2exlem  3212  spc3gv  3508  vn0  4227  notzfaus  5228  notzfausOLD  5229  dtru  5237  dvdemo1  5240  dtruALT  5255  eunex  5257  reusv2lem2  5266  dtruALT2  5302  brprcneu  6665  fvprc  6666  dffv2  6763  zfcndpow  10116  hashfun  13890  nmo  30412  bnj1304  32370  bnj1253  32568  axrepprim  33214  axunprim  33215  axregprim  33217  axinfprim  33218  axacprim  33219  dftr6  33289  brtxpsd  33834  elfuns  33855  dfrdg4  33891  bj-dtru  34630  relowlpssretop  35158  sn-dtru  39779  clsk3nimkb  41196  expandexn  41449  vk15.4j  41686  vk15.4jVD  42072  alneu  44149