Metamath Proof Explorer

Theorem elblps

Description: Membership in a ball. (Contributed by NM, 2-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013) (Revised by Thierry Arnoux, 11-Mar-2018)

		Ref	Expression
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		blvalps	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R = \{x \in X \| P D x < R\}$
2	1	eleq2d	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \to (A \in (P ball (D) R) \leftrightarrow A \in \{x \in X \| P D x < R\})$
3		oveq2	$⊢ x = A \to P D x = P D A$
4	3	breq1d	$⊢ x = A \to (P D x < R \leftrightarrow P D A < R)$
5	4	elrab	$⊢ A \in \{x \in X \| P D x < R\} \leftrightarrow (A \in X \land P D A < R)$
6	2 5	bitrdi	$⊢ (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))$