![]() |
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 395 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) | |
2 | 1 | exbii 1811 | . 2 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑 → 𝜓)) |
3 | exnal 1790 | . 2 ⊢ (∃𝑥 ¬ (𝜑 → 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) | |
4 | 2, 3 | bitri 267 | 1 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 ∀wal 1506 ∃wex 1743 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1744 |
This theorem is referenced by: sbnvOLD 2246 sbnOLD 2463 sbnALT 2523 gencbval 3465 dfss6 3841 nss 3912 nssss 5201 brprcneu 6488 marypha1lem 8690 reclem2pr 10266 dftr6 32543 brsset 32908 dfon3 32911 dffun10 32933 elfuns 32934 ecinn0 35090 ax12indn 35561 expandrexn 40040 vk15.4j 40318 vk15.4jVD 40704 |
Copyright terms: Public domain | W3C validator |