![]() |
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 403 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) | |
2 | 1 | exbii 1845 | . 2 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑 → 𝜓)) |
3 | exnal 1824 | . 2 ⊢ (∃𝑥 ¬ (𝜑 → 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) | |
4 | 2, 3 | bitri 275 | 1 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1535 ∃wex 1776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 |
This theorem is referenced by: gencbval 3543 dfss6 3985 nss 4060 nssss 5466 brprcneu 6897 brprcneuALT 6898 marypha1lem 9471 reclem2pr 11086 dftr6 35731 brsset 35871 dfon3 35874 dffun10 35896 elfuns 35897 ecinn0 38335 ax12indn 38925 expandrexn 44287 vk15.4j 44526 vk15.4jVD 44912 |
Copyright terms: Public domain | W3C validator |