Description: Version of 19.23 with a disjoint variable condition instead of a non-freeness hypothesis. (Contributed by NM, 28-Jun-1998) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020) Remove dependency on ax-6 . (Revised by Rohan Ridenour, 15-Apr-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 19.23v | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 𝜑 → 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exim | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) | |
| 2 | ax5e | ⊢ ( ∃ 𝑥 𝜓 → 𝜓 ) | |
| 3 | 1 2 | syl6 | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → 𝜓 ) ) |
| 4 | ax-5 | ⊢ ( 𝜓 → ∀ 𝑥 𝜓 ) | |
| 5 | 4 | imim2i | ⊢ ( ( ∃ 𝑥 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ) |
| 6 | 19.38 | ⊢ ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) | |
| 7 | 5 6 | syl | ⊢ ( ( ∃ 𝑥 𝜑 → 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) |
| 8 | 3 7 | impbii | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 𝜑 → 𝜓 ) ) |