Theorem exnal 1828

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1536  ∃wex 1781

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

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  alexn  1846  exanali  1860  19.35  1878  19.30  1882  nfeqf2  2384  nabbi  3089  r2exlem  3261  spc3gv  3553  notzfaus  5227  notzfausOLD  5228  dtru  5236  dvdemo1  5239  dtruALT  5254  eunex  5256  reusv2lem2  5265  dtruALT2  5301  brprcneu  6637  dffv2  6733  zfcndpow  10027  hashfun  13794  nmo  30261  bnj1304  32201  bnj1253  32399  axrepprim  33041  axunprim  33042  axregprim  33044  axinfprim  33045  axacprim  33046  dftr6  33099  brtxpsd  33468  elfuns  33489  dfrdg4  33525  bj-dtru  34254  relowlpssretop  34781  sn-dtru  39403  clsk3nimkb  40743  expandexn  40997  vk15.4j  41234  vk15.4jVD  41620  alneu  43680