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  2411  nabbib  3065  r2exlem  3156  spc3gv  3565  vn0OLD  4299  notsep  5336  dtruALT2  5343  dvdemo1  5346  dtruALT  5361  eunex  5363  reusv2lem2  5372  dtru  5420  brprcneu  6875  brprcneuALT  6876  dffv2  6980  zfcndpow  10612  hashfun  14488  nmo  32883  bnj1304  35248  bnj1253  35446  axregs  35585  onvf1odlem4  35623  axrepprim  36207  axunprim  36208  axregprim  36210  axinfprim  36211  axacprim  36212  dftr6  36256  brtxpsd  36397  elfuns  36418  dfrdg4  36456  bj-cbvaw  37296  relowlpssretop  38043  onsupmaxb  43999  clsk3nimkb  44799  expandexn  45032  vk15.4j  45270  vk15.4jVD  45655  alneu  47894