elbl2ps

Description: Membership in a ball. (Contributed by NM, 9-Mar-2007) (Revised by Thierry Arnoux, 11-Mar-2018)

		Ref	Expression
	Assertion	elbl2ps	$⊢ ((D \in PsMet (X) \land R \in ℝ^{*}) \land (P \in X \land A \in X)) \to (A \in (P ball (D) R) \leftrightarrow P D A < R)$

Step	Hyp	Ref	Expression
1		simprr	$⊢ ((D \in PsMet (X) \land R \in ℝ^{*}) \land (P \in X \land A \in X)) \to A \in X$
2		elblps	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \to (A \in (P ball (D) R) \leftrightarrow (A \in X \land P D A < R))$
3	2	3expa	$⊢ ((D \in PsMet (X) \land P \in X) \land R \in ℝ^{*}) \to (A \in (P ball (D) R) \leftrightarrow (A \in X \land P D A < R))$
4	3	an32s	$⊢ ((D \in PsMet (X) \land R \in ℝ^{*}) \land P \in X) \to (A \in (P ball (D) R) \leftrightarrow (A \in X \land P D A < R))$
5	4	adantrr	$⊢ ((D \in PsMet (X) \land R \in ℝ^{*}) \land (P \in X \land A \in X)) \to (A \in (P ball (D) R) \leftrightarrow (A \in X \land P D A < R))$
6	1 5	mpbirand	$⊢ ((D \in PsMet (X) \land R \in ℝ^{*}) \land (P \in X \land A \in X)) \to (A \in (P ball (D) R) \leftrightarrow P D A < R)$

Metamath Proof Explorer