Description: Theorem 19.22 of Margaris p. 90. (Contributed by NM, 10-Jan-1993) (Proof shortened by Wolf Lammen, 4-Jul-2014) Prove it directly from alim to allow use in bj-alexim . (Revised by BJ, 9-Dec-2023) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-exim | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | con3 | ⊢ ( ( 𝜑 → 𝜓 ) → ( ¬ 𝜓 → ¬ 𝜑 ) ) | |
| 2 | 1 | alimi | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ∀ 𝑥 ( ¬ 𝜓 → ¬ 𝜑 ) ) |
| 3 | alim | ⊢ ( ∀ 𝑥 ( ¬ 𝜓 → ¬ 𝜑 ) → ( ∀ 𝑥 ¬ 𝜓 → ∀ 𝑥 ¬ 𝜑 ) ) | |
| 4 | con3 | ⊢ ( ( ∀ 𝑥 ¬ 𝜓 → ∀ 𝑥 ¬ 𝜑 ) → ( ¬ ∀ 𝑥 ¬ 𝜑 → ¬ ∀ 𝑥 ¬ 𝜓 ) ) | |
| 5 | 2 3 4 | 3syl | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ¬ ∀ 𝑥 ¬ 𝜑 → ¬ ∀ 𝑥 ¬ 𝜓 ) ) |
| 6 | df-ex | ⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 ) | |
| 7 | df-ex | ⊢ ( ∃ 𝑥 𝜓 ↔ ¬ ∀ 𝑥 ¬ 𝜓 ) | |
| 8 | 5 6 7 | 3imtr4g | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) |