![]() |
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 404 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) | |
2 | 1 | exbii 1850 | . 2 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑 → 𝜓)) |
3 | exnal 1829 | . 2 ⊢ (∃𝑥 ¬ (𝜑 → 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) | |
4 | 2, 3 | bitri 274 | 1 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∀wal 1539 ∃wex 1781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 |
This theorem is referenced by: gencbval 3537 dfss6 3971 nss 4046 nssss 5455 brprcneu 6881 brprcneuALT 6882 marypha1lem 9427 reclem2pr 11042 dftr6 34716 brsset 34856 dfon3 34859 dffun10 34881 elfuns 34882 ecinn0 37217 ax12indn 37808 expandrexn 43040 vk15.4j 43279 vk15.4jVD 43665 |
Copyright terms: Public domain | W3C validator |