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 e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A e. X /\ ( P D A ) < R ) ) )

Proof

Step	Hyp	Ref	Expression
1		blvalps	|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) = { x e. X | ( P D x ) < R } )
2	1	eleq2d	|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( A e. ( P ( ball ` D ) R ) <-> A e. { x e. X | ( P D x ) < R } ) )
3		oveq2	|- ( x = A -> ( P D x ) = ( P D A ) )
4	3	breq1d	|- ( x = A -> ( ( P D x ) < R <-> ( P D A ) < R ) )
5	4	elrab	|- ( A e. { x e. X | ( P D x ) < R } <-> ( A e. X /\ ( P D A ) < R ) )
6	2 5	bitrdi	|- ( ( D e. ( PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A e. X /\ ( P D A ) < R ) ) )