![]() |
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 1875 | . . 3 ⊢ (∀𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓)) |
3 | 2 | com12 32 | . 2 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓)) |
4 | exnal 1870 | . . . 4 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) | |
5 | pm2.21 121 | . . . . 5 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | |
6 | 5 | eximi 1878 | . . . 4 ⊢ (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑 → 𝜓)) |
7 | 4, 6 | sylbir 227 | . . 3 ⊢ (¬ ∀𝑥𝜑 → ∃𝑥(𝜑 → 𝜓)) |
8 | exa1 1881 | . . 3 ⊢ (∃𝑥𝜓 → ∃𝑥(𝜑 → 𝜓)) | |
9 | 7, 8 | ja 175 | . 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓)) |
10 | 3, 9 | impbii 201 | 1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∀wal 1599 ∃wex 1823 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 |
This theorem depends on definitions: df-bi 199 df-ex 1824 |
This theorem is referenced by: 19.35i 1925 19.35ri 1926 19.25 1927 19.43 1929 nfimd 1940 19.36imv 1988 19.37imv 1990 speimfwALT 2008 19.39 2033 19.24 2034 19.36v 2036 19.37v 2040 19.36 2216 19.37 2218 spimt 2350 spimtOLD 2351 grothprim 9991 bj-nfimt 33196 bj-spimt2 33297 bj-spimtv 33306 bj-snsetex 33523 |
Copyright terms: Public domain | W3C validator |