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 1823 | . . 3 ⊢ (∀𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓)) |
3 | 2 | com12 32 | . 2 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓)) |
4 | exnal 1818 | . . . 4 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) | |
5 | pm2.21 123 | . . . . 5 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | |
6 | 5 | eximi 1826 | . . . 4 ⊢ (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑 → 𝜓)) |
7 | 4, 6 | sylbir 236 | . . 3 ⊢ (¬ ∀𝑥𝜑 → ∃𝑥(𝜑 → 𝜓)) |
8 | exa1 1829 | . . 3 ⊢ (∃𝑥𝜓 → ∃𝑥(𝜑 → 𝜓)) | |
9 | 7, 8 | ja 187 | . 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓)) |
10 | 3, 9 | impbii 210 | 1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∀wal 1526 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: 19.35i 1870 19.35ri 1871 19.25 1872 19.43 1874 nfimd 1886 19.36imv 1937 19.37imv 1939 speimfwALT 1958 19.39 1982 19.24 1983 19.36v 1985 19.37v 1989 19.36 2222 19.37 2224 spimt 2395 grothprim 10244 bj-nfimt 33868 bj-nnfim 33972 bj-19.36im 33997 bj-19.37im 33998 bj-spimt2 34004 bj-spimtv 34013 |
Copyright terms: Public domain | W3C validator |