![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exanali | Structured version Visualization version GIF version |
Description: A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996.) (Proof shortened by Wolf Lammen, 4-Sep-2014.) |
Ref | Expression |
---|---|
exanali | ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | annim 390 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) | |
2 | 1 | exbii 1923 | . 2 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑 → 𝜓)) |
3 | exnal 1901 | . 2 ⊢ (∃𝑥 ¬ (𝜑 → 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) | |
4 | 2, 3 | bitri 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 |