Description: A condition allowing to swap an existential quantifier and a unique existential quantifier. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker 2euswapv when possible. (Contributed by NM, 10-Apr-2004) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 2euswap | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃! 𝑥 ∃ 𝑦 𝜑 → ∃! 𝑦 ∃ 𝑥 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | excomim | ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 → ∃ 𝑦 ∃ 𝑥 𝜑 ) | |
| 2 | 1 | a1i | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃ 𝑥 ∃ 𝑦 𝜑 → ∃ 𝑦 ∃ 𝑥 𝜑 ) ) |
| 3 | 2moswap | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃* 𝑥 ∃ 𝑦 𝜑 → ∃* 𝑦 ∃ 𝑥 𝜑 ) ) | |
| 4 | 2 3 | anim12d | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑥 ∃ 𝑦 𝜑 ) → ( ∃ 𝑦 ∃ 𝑥 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) ) ) |
| 5 | df-eu | ⊢ ( ∃! 𝑥 ∃ 𝑦 𝜑 ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑥 ∃ 𝑦 𝜑 ) ) | |
| 6 | df-eu | ⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 ↔ ( ∃ 𝑦 ∃ 𝑥 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) ) | |
| 7 | 4 5 6 | 3imtr4g | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃! 𝑥 ∃ 𝑦 𝜑 → ∃! 𝑦 ∃ 𝑥 𝜑 ) ) |