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 | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) |