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

Theorem exanali 1946
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 392 . . 3 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
21exbii 1933 . 2 (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑𝜓))
3 exnal 1911 . 2 (∃𝑥 ¬ (𝜑𝜓) ↔ ¬ ∀𝑥(𝜑𝜓))
42, 3bitri 266 1 (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wal 1635  wex 1859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860
This theorem is referenced by:  sbn  2550  gencbval  3446  dfss6  3788  nss  3860  nssss  5114  brprcneu  6396  marypha1lem  8574  reclem2pr  10151  dftr6  31960  brsset  32315  dfon3  32318  dffun10  32340  elfuns  32341  ecinn0  34429  ax12indn  34720  vk15.4j  39229  vk15.4jVD  39641
  Copyright terms: Public domain W3C validator