![]() |
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 1900 | . . 3 ⊢ (∀𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓)) |
3 | 2 | com12 32 | . 2 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓)) |
4 | exnal 1895 | . . . 4 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) | |
5 | pm2.21 120 | . . . . 5 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | |
6 | 5 | eximi 1903 | . . . 4 ⊢ (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑 → 𝜓)) |
7 | 4, 6 | sylbir 225 | . . 3 ⊢ (¬ ∀𝑥𝜑 → ∃𝑥(𝜑 → 𝜓)) |
8 | exa1 1906 | . . 3 ⊢ (∃𝑥𝜓 → ∃𝑥(𝜑 → 𝜓)) | |
9 | 7, 8 | ja 173 | . 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓)) |
10 | 3, 9 | impbii 199 | 1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∀wal 1622 ∃wex 1845 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 |
This theorem depends on definitions: df-bi 197 df-ex 1846 |
This theorem is referenced by: 19.35i 1947 19.35ri 1948 19.25 1949 19.43 1951 nfimt 1962 nfimdOLDOLD 1965 19.36imv 2014 19.37imv 2016 speimfwALT 2035 19.39 2057 19.24 2058 19.36v 2061 19.37v 2067 19.36 2237 19.37 2239 spimt 2390 grothprim 9840 bj-spimt2 33007 bj-spimtv 33016 bj-snsetex 33249 |
Copyright terms: Public domain | W3C validator |