Description: A condition allowing to swap an existential quantifier and a unique existential quantifier. Version of 2euswap with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 10-Apr-2004) (Revised by GG, 22-Aug-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 2euswapv | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃! 𝑥 ∃ 𝑦 𝜑 → ∃! 𝑦 ∃ 𝑥 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | excomim | ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 → ∃ 𝑦 ∃ 𝑥 𝜑 ) | |
| 2 | 1 | a1i | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃ 𝑥 ∃ 𝑦 𝜑 → ∃ 𝑦 ∃ 𝑥 𝜑 ) ) |
| 3 | 2moswapv | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃* 𝑥 ∃ 𝑦 𝜑 → ∃* 𝑦 ∃ 𝑥 𝜑 ) ) | |
| 4 | 2 3 | anim12d | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑥 ∃ 𝑦 𝜑 ) → ( ∃ 𝑦 ∃ 𝑥 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) ) ) |
| 5 | df-eu | ⊢ ( ∃! 𝑥 ∃ 𝑦 𝜑 ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑥 ∃ 𝑦 𝜑 ) ) | |
| 6 | df-eu | ⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 ↔ ( ∃ 𝑦 ∃ 𝑥 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) ) | |
| 7 | 4 5 6 | 3imtr4g | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃! 𝑥 ∃ 𝑦 𝜑 → ∃! 𝑦 ∃ 𝑥 𝜑 ) ) |