|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > 19.35 | Structured version Visualization version GIF version | ||
| Description: Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.) | 
| Ref | Expression | 
|---|---|
| 19.35 | ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | pm2.27 42 | . . . 4 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓)) | |
| 2 | 1 | aleximi 1832 | . . 3 ⊢ (∀𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓)) | 
| 3 | 2 | com12 32 | . 2 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓)) | 
| 4 | exnal 1827 | . . . 4 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) | |
| 5 | pm2.21 123 | . . . . 5 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | |
| 6 | 5 | eximi 1835 | . . . 4 ⊢ (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑 → 𝜓)) | 
| 7 | 4, 6 | sylbir 235 | . . 3 ⊢ (¬ ∀𝑥𝜑 → ∃𝑥(𝜑 → 𝜓)) | 
| 8 | exa1 1838 | . . 3 ⊢ (∃𝑥𝜓 → ∃𝑥(𝜑 → 𝜓)) | |
| 9 | 7, 8 | ja 186 | . 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓)) | 
| 10 | 3, 9 | impbii 209 | 1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∀wal 1538 ∃wex 1779 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 | 
| This theorem depends on definitions: df-bi 207 df-ex 1780 | 
| This theorem is referenced by: 19.35i 1878 19.35ri 1879 19.25 1880 19.43 1882 nfimd 1894 19.37imv 1947 speimfwALT 1964 19.39 1984 19.24 1985 19.36v 1987 19.37v 1991 19.36 2230 19.37 2232 spimt 2391 grothprim 10874 bj-nfimt 36639 bj-nnfim 36747 bj-19.36im 36772 bj-19.37im 36773 bj-spimt2 36786 bj-spimtv 36795 | 
| Copyright terms: Public domain | W3C validator |