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  1912  19.30  1916  nfeqf2  2409  nabbib  3064  r2exlem  3155  spc3gv  3562  vn0OLD  4295  notsep  5332  dtruALT2  5339  dvdemo1  5342  dtruALT  5357  eunex  5359  reusv2lem2  5368  dtru  5412  brprcneu  6906  brprcneuALT  6907  dffv2  7011  zfcndpow  10740  hashfun  14623  degenmgm2nfun  19189  nmo  33185  bnj1304  35560  bnj1253  35758  axregs  35948  onvf1odlem4  36075  mirimanofffr  36670  axrepprim  36682  axunprim  36683  axregprim  36685  axinfprim  36686  axacprim  36687  dftr6  36731  brtxpsd  36871  elfuns  36892  dfrdg4  36930  bj-cbvaw  37755  relowlpssretop  38555  onsupmaxb  44502  clsk3nimkb  45301  expandexn  45534  vk15.4j  45771  vk15.4jVD  46156  alneu  48467