Metamath Proof Explorer

Theorem elbl2

Description: Membership in a ball. (Contributed by NM, 9-Mar-2007)

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

Proof

Step Hyp Ref Expression
1 simprr ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ X
2 elbl ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → A ∈ P ball ⁡ D R ↔ A ∈ X ∧ P D A < R
3 2 3expa ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → A ∈ P ball ⁡ D R ↔ A ∈ X ∧ P D A < R
4 3 an32s ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X → A ∈ P ball ⁡ D R ↔ A ∈ X ∧ P D A < R
5 4 adantrr ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ A ∈ X ∧ P D A < R
6 1 5 mpbirand ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ P D A < R