Theorem exnal 1827

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538  ∃wex 1779

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

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

This theorem is referenced by:  alexn  1845  nfnbi  1855  exanali  1859  19.35  1877  19.30  1881  nfeqf2  2382  nabbib  3045  r2exlem  3143  spc3gv  3604  vn0  4345  notzfaus  5363  dtruALT2  5370  dvdemo1  5373  dtruALT  5388  eunex  5390  reusv2lem2  5399  dtru  5441  dtruOLD  5446  brprcneu  6896  brprcneuALT  6897  dffv2  7004  zfcndpow  10656  hashfun  14476  nmo  32509  bnj1304  34833  bnj1253  35031  axrepprim  35702  axunprim  35703  axregprim  35705  axinfprim  35706  axacprim  35707  dftr6  35751  brtxpsd  35895  elfuns  35916  dfrdg4  35952  relowlpssretop  37365  onsupmaxb  43251  clsk3nimkb  44053  expandexn  44308  vk15.4j  44548  vk15.4jVD  44934  alneu  47136