elbl

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

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

Step	Hyp	Ref	Expression
1		blval	$⊢ (D \in ∞Met (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 ∞Met (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 ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (A \in (P ball (D) R) \leftrightarrow (A \in X \land P D A < R))$

Metamath Proof Explorer