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

Theorem exanali 1854
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 403 . . 3 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
21exbii 1842 . 2 (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑𝜓))
3 exnal 1821 . 2 (∃𝑥 ¬ (𝜑𝜓) ↔ ¬ ∀𝑥(𝜑𝜓))
42, 3bitri 275 1 (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wal 1531  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774
This theorem is referenced by:  gencbval  3530  dfss6  3964  nss  4039  nssss  5446  brprcneu  6872  brprcneuALT  6873  marypha1lem  9425  reclem2pr  11040  dftr6  35217  brsset  35357  dfon3  35360  dffun10  35382  elfuns  35383  ecinn0  37716  ax12indn  38307  expandrexn  43564  vk15.4j  43803  vk15.4jVD  44189
  Copyright terms: Public domain W3C validator