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∈Pball⁡DR↔PDA<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∈Pball⁡DR↔A∈X∧PDA<R
3 2 3expa ⊢D∈∞Met⁡X∧P∈X∧R∈ℝ*→A∈Pball⁡DR↔A∈X∧PDA<R
4 3 an32s ⊢D∈∞Met⁡X∧R∈ℝ*∧P∈X→A∈Pball⁡DR↔A∈X∧PDA<R
5 4 adantrr ⊢D∈∞Met⁡X∧R∈ℝ*∧P∈X∧A∈X→A∈Pball⁡DR↔A∈X∧PDA<R
6 1 5 mpbirand ⊢D∈∞Met⁡X∧R∈ℝ*∧P∈X∧A∈X→A∈Pball⁡DR↔PDA<R