Theorem exnal 1903

Description: 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 1902	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
2	1	con2bii 346	1 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 196  ∀wal 1630  ∃wex 1853

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

This theorem depends on definitions:  df-bi 197  df-ex 1854

This theorem is referenced by:  alexn  1920  exanali  1935  19.35  1954  19.30  1958  nfeqf2  2442  nabbi  3034  r2exlem  3197  spc3gv  3438  notzfaus  4989  dtru  5006  eunex  5008  reusv2lem2  5018  reusv2lem2OLD  5019  dtruALT  5048  dvdemo1  5051  dtruALT2  5060  brprcneu  6345  dffv2  6433  zfcndpow  9630  hashfun  13416  nmo  29634  bnj1304  31197  bnj1253  31392  axrepprim  31886  axunprim  31887  axregprim  31889  axinfprim  31890  axacprim  31891  dftr6  31947  brtxpsd  32307  elfuns  32328  dfrdg4  32364  bj-dtru  33103  bj-eunex  33105  bj-dvdemo1  33108  relowlpssretop  33523  wl-dveeq12  33624  clsk3nimkb  38840  vk15.4j  39236  vk15.4jVD  39649  alneu  41707