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 | ||
|---|---|---|---|
| Assertion | 19.35 | ⊢ ( ∃ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm2.27 | ⊢ ( 𝜑 → ( ( 𝜑 → 𝜓 ) → 𝜓 ) ) | |
| 2 | 1 | aleximi | ⊢ ( ∀ 𝑥 𝜑 → ( ∃ 𝑥 ( 𝜑 → 𝜓 ) → ∃ 𝑥 𝜓 ) ) |
| 3 | 2 | com12 | ⊢ ( ∃ 𝑥 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) |
| 4 | exnal | ⊢ ( ∃ 𝑥 ¬ 𝜑 ↔ ¬ ∀ 𝑥 𝜑 ) | |
| 5 | pm2.21 | ⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) ) | |
| 6 | 5 | eximi | ⊢ ( ∃ 𝑥 ¬ 𝜑 → ∃ 𝑥 ( 𝜑 → 𝜓 ) ) |
| 7 | 4 6 | sylbir | ⊢ ( ¬ ∀ 𝑥 𝜑 → ∃ 𝑥 ( 𝜑 → 𝜓 ) ) |
| 8 | exa1 | ⊢ ( ∃ 𝑥 𝜓 → ∃ 𝑥 ( 𝜑 → 𝜓 ) ) | |
| 9 | 7 8 | ja | ⊢ ( ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) → ∃ 𝑥 ( 𝜑 → 𝜓 ) ) |
| 10 | 3 9 | impbii | ⊢ ( ∃ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) |