MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exanali Structured version   Visualization version   GIF version

Theorem exanali 1783
Description: A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996.) (Proof shortened by Wolf Lammen, 4-Sep-2014.)
Assertion
Ref Expression
exanali (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑𝜓))

Proof of Theorem exanali
StepHypRef Expression
1 annim 441 . . 3 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
21exbii 1771 . 2 (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑𝜓))
3 exnal 1751 . 2 (∃𝑥 ¬ (𝜑𝜓) ↔ ¬ ∀𝑥(𝜑𝜓))
42, 3bitri 264 1 (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wal 1478  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702
This theorem is referenced by:  sbn  2390  gencbval  3242  nss  3648  nssss  4895  brprcneu  6151  marypha1lem  8299  reclem2pr  9830  dftr6  31401  brsset  31691  dfon3  31694  dffun10  31716  elfuns  31717  ax12indn  33747  dfss6  37583  vk15.4j  38255  vk15.4jVD  38672
  Copyright terms: Public domain W3C validator