![]() |
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 1835 | . . 3 ⊢ (∀𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓)) |
3 | 2 | com12 32 | . 2 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓)) |
4 | exnal 1830 | . . . 4 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) | |
5 | pm2.21 123 | . . . . 5 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | |
6 | 5 | eximi 1838 | . . . 4 ⊢ (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑 → 𝜓)) |
7 | 4, 6 | sylbir 234 | . . 3 ⊢ (¬ ∀𝑥𝜑 → ∃𝑥(𝜑 → 𝜓)) |
8 | exa1 1841 | . . 3 ⊢ (∃𝑥𝜓 → ∃𝑥(𝜑 → 𝜓)) | |
9 | 7, 8 | ja 186 | . 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓)) |
10 | 3, 9 | impbii 208 | 1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∀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-ex 1783 |
This theorem is referenced by: 19.35i 1882 19.35ri 1883 19.25 1884 19.43 1886 nfimd 1898 19.36imvOLD 1950 19.37imv 1952 speimfwALT 1969 19.39 1989 19.24 1990 19.36v 1992 19.37v 1996 19.36 2224 19.37 2226 spimt 2386 grothprim 10826 bj-nfimt 35504 bj-nnfim 35613 bj-19.36im 35638 bj-19.37im 35639 bj-spimt2 35652 bj-spimtv 35661 |
Copyright terms: Public domain | W3C validator |