Description: A condition allowing to swap an existential quantifier and at at-most-one quantifier. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker 2moswapv when possible. (Contributed by NM, 10-Apr-2004) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 2moswap | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃* 𝑥 ∃ 𝑦 𝜑 → ∃* 𝑦 ∃ 𝑥 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfe1 | ⊢ Ⅎ 𝑦 ∃ 𝑦 𝜑 | |
| 2 | 1 | moexex | ⊢ ( ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) → ∃* 𝑦 ∃ 𝑥 ( ∃ 𝑦 𝜑 ∧ 𝜑 ) ) |
| 3 | 2 | expcom | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃* 𝑥 ∃ 𝑦 𝜑 → ∃* 𝑦 ∃ 𝑥 ( ∃ 𝑦 𝜑 ∧ 𝜑 ) ) ) |
| 4 | 19.8a | ⊢ ( 𝜑 → ∃ 𝑦 𝜑 ) | |
| 5 | 4 | pm4.71ri | ⊢ ( 𝜑 ↔ ( ∃ 𝑦 𝜑 ∧ 𝜑 ) ) |
| 6 | 5 | exbii | ⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ( ∃ 𝑦 𝜑 ∧ 𝜑 ) ) |
| 7 | 6 | mobii | ⊢ ( ∃* 𝑦 ∃ 𝑥 𝜑 ↔ ∃* 𝑦 ∃ 𝑥 ( ∃ 𝑦 𝜑 ∧ 𝜑 ) ) |
| 8 | 3 7 | imbitrrdi | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃* 𝑥 ∃ 𝑦 𝜑 → ∃* 𝑦 ∃ 𝑥 𝜑 ) ) |