Metamath Proof Explorer

Theorem elrng

Description: Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011)

Ref Expression
Assertion elrng 
|- ( A e. V -> ( A e. ran B <-> E. x x B A ) )

Proof

Step Hyp Ref Expression
1 elrn2g 
 |-  ( A e. V -> ( A e. ran B <-> E. x <. x , A >. e. B ) )
2 df-br 
 |-  ( x B A <-> <. x , A >. e. B )
3 2 exbii 
 |-  ( E. x x B A <-> E. x <. x , A >. e. B )
4 1 3 bitr4di 
 |-  ( A e. V -> ( A e. ran B <-> E. x x B A ) )