Metamath Proof Explorer

Theorem elbl

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

Ref Expression
Assertion elbl 
|- ( ( D e. ( *Met ` 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 blval 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) = { x e. X | ( P D x ) < R } )
2 1 eleq2d 
 |-  ( ( D e. ( *Met ` 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. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A e. X /\ ( P D A ) < R ) ) )