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

Theorem exanali 1822
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 395 . . 3 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
21exbii 1811 . 2 (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑𝜓))
3 exnal 1790 . 2 (∃𝑥 ¬ (𝜑𝜓) ↔ ¬ ∀𝑥(𝜑𝜓))
42, 3bitri 267 1 (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  wal 1506  wex 1743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744
This theorem is referenced by:  sbnvOLD  2246  sbnOLD  2463  sbnALT  2523  gencbval  3465  dfss6  3841  nss  3912  nssss  5201  brprcneu  6488  marypha1lem  8690  reclem2pr  10266  dftr6  32543  brsset  32908  dfon3  32911  dffun10  32933  elfuns  32934  ecinn0  35090  ax12indn  35561  expandrexn  40040  vk15.4j  40318  vk15.4jVD  40704
  Copyright terms: Public domain W3C validator