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  2375  nabbib  3028  r2exlem  3118  spc3gv  3559  vn0  4296  notzfaus  5302  dtruALT2  5309  dvdemo1  5312  dtruALT  5327  eunex  5329  reusv2lem2  5338  dtru  5380  brprcneu  6812  brprcneuALT  6813  dffv2  6918  zfcndpow  10510  hashfun  14344  nmo  32434  bnj1304  34792  bnj1253  34990  axregs  35084  onvf1odlem4  35089  axrepprim  35685  axunprim  35686  axregprim  35688  axinfprim  35689  axacprim  35690  dftr6  35734  brtxpsd  35878  elfuns  35899  dfrdg4  35935  relowlpssretop  37348  onsupmaxb  43222  clsk3nimkb  44023  expandexn  44272  vk15.4j  44512  vk15.4jVD  44897  alneu  47118