Description: Alternate proof of exim directly from alim by using df-ex (using duality of A. and E. . (Contributed by BJ, 9-Dec-2023) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-eximALT | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) |
| 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 | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) |