![]() |
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 405 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) | |
2 | 1 | exbii 1851 | . 2 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑 → 𝜓)) |
3 | exnal 1830 | . 2 ⊢ (∃𝑥 ¬ (𝜑 → 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) | |
4 | 2, 3 | bitri 275 | 1 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∀wal 1540 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 |
This theorem is referenced by: gencbval 3538 dfss6 3972 nss 4047 nssss 5456 brprcneu 6882 brprcneuALT 6883 marypha1lem 9428 reclem2pr 11043 dftr6 34752 brsset 34892 dfon3 34895 dffun10 34917 elfuns 34918 ecinn0 37270 ax12indn 37861 expandrexn 43098 vk15.4j 43337 vk15.4jVD 43723 |
Copyright terms: Public domain | W3C validator |