Theorem exnal 1744

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

Syntax hints:  ¬ wn 3   ↔ wb 195  ∀wal 1473  ∃wex 1695

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

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  alexn  1760  exanali  1773  19.35  1794  19.30  1798  nfeqf2  2285  nabbi  2884  r2exlem  3041  spc3gv  3271  notzfaus  4766  dtru  4783  eunex  4785  reusv2lem2  4795  reusv2lem2OLD  4796  dtruALT  4826  dvdemo1  4829  dtruALT2  4838  brprcneu  6096  dffv2  6181  zfcndpow  9317  hashfun  13084  nmo  28709  bnj1304  30144  bnj1253  30339  axrepprim  30833  axunprim  30834  axregprim  30836  axinfprim  30837  axacprim  30838  dftr6  30893  brtxpsd  31171  elfuns  31192  dfrdg4  31228  bj-dtru  31985  bj-eunex  31987  bj-dvdemo1  31990  relowlpssretop  32388  wl-dveeq12  32490  clsk3nimkb  37358  vk15.4j  37755  vk15.4jVD  38172  alneu  39850