|   | 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 1847 | . 2 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ∃𝑥 ¬ (𝜑 → 𝜓)) | 
| 3 | exnal 1826 | . 2 ⊢ (∃𝑥 ¬ (𝜑 → 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) | |
| 4 | 2, 3 | bitri 275 | 1 ⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1537 ∃wex 1778 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 | 
| This theorem is referenced by: gencbval 3542 dfss6 3972 nss 4047 nssss 5459 brprcneu 6895 brprcneuALT 6896 marypha1lem 9474 reclem2pr 11089 dftr6 35752 brsset 35891 dfon3 35894 dffun10 35916 elfuns 35917 ecinn0 38355 ax12indn 38945 expandrexn 44315 vk15.4j 44553 vk15.4jVD 44939 | 
| Copyright terms: Public domain | W3C validator |