Metamath Proof Explorer

Theorem blcom

Description: Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014)

Ref Expression
Assertion blcom ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ P ∈ A ball ⁡ D R

Proof

Step Hyp Ref Expression
1 elbl2 ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ P D A < R
2 elbl3 ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ A ∈ X ∧ P ∈ X → P ∈ A ball ⁡ D R ↔ P D A < R
3 2 ancom2s ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → P ∈ A ball ⁡ D R ↔ P D A < R
4 1 3 bitr4d ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ P ∈ A ball ⁡ D R