Theorem exnal 1860

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  alexn  1878  nfnbi  1888  exanali  1892  19.35  1910  19.30  1914  nfeqf2  2406  nabbib  3060  r2exlem  3151  spc3gv  3558  vn0OLD  4292  notsep  5328  dtruALT2  5335  dvdemo1  5338  dtruALT  5353  eunex  5355  reusv2lem2  5364  dtru  5412  brprcneu  6868  brprcneuALT  6869  dffv2  6973  zfcndpow  10625  hashfun  14502  degenmgm2nfun  19052  nmo  32965  bnj1304  35328  bnj1253  35526  axregs  35665  onvf1odlem4  35703  axrepprim  36281  axunprim  36282  axregprim  36284  axinfprim  36285  axacprim  36286  dftr6  36330  brtxpsd  36471  elfuns  36492  dfrdg4  36530  bj-cbvaw  37371  relowlpssretop  38118  onsupmaxb  44080  clsk3nimkb  44880  expandexn  45113  vk15.4j  45351  vk15.4jVD  45736  alneu  48012