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

Theorem exanali 1936
 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 390 . . 3 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
21exbii 1923 . 2 (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑𝜓))
3 exnal 1901 . 2 (∃𝑥 ¬ (𝜑𝜓) ↔ ¬ ∀𝑥(𝜑𝜓))
42, 3bitri 264 1 (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382  ∀wal 1628  ∃wex 1851 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884 This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1852 This theorem is referenced by:  sbn  2537  gencbval  3401  dfss6  3740  nss  3810  nssss  5052  brprcneu  6325  marypha1lem  8494  reclem2pr  10071  dftr6  31972  brsset  32327  dfon3  32330  dffun10  32352  elfuns  32353  ecinn0  34453  ax12indn  34744  vk15.4j  39253  vk15.4jVD  39666
 Copyright terms: Public domain W3C validator