Description: Membership in a range. (Contributed by NM, 2Apr2004)
Ref  Expression  

Hypothesis  elrn.1   A e. _V 

Assertion  elrn   ( A e. ran B <> E. x x B A ) 
Step  Hyp  Ref  Expression 

1  elrn.1   A e. _V 

2  1  elrn2   ( A e. ran B <> E. x <. x , A >. e. B ) 
3  dfbr   ( x B A <> <. x , A >. e. B ) 

4  3  exbii   ( E. x x B A <> E. x <. x , A >. e. B ) 
5  2 4  bitr4i   ( A e. ran B <> E. x x B A ) 