Description: Membership in a range. (Contributed by NM, 10-Jul-1994)
Ref | Expression | ||
---|---|---|---|
Hypothesis | elrn.1 | |- A e. _V |
|
Assertion | elrn2 | |- ( A e. ran B <-> E. x <. x , A >. e. B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrn.1 | |- A e. _V |
|
2 | opeq2 | |- ( y = A -> <. x , y >. = <. x , A >. ) |
|
3 | 2 | eleq1d | |- ( y = A -> ( <. x , y >. e. B <-> <. x , A >. e. B ) ) |
4 | 3 | exbidv | |- ( y = A -> ( E. x <. x , y >. e. B <-> E. x <. x , A >. e. B ) ) |
5 | dfrn3 | |- ran B = { y | E. x <. x , y >. e. B } |
|
6 | 1 4 5 | elab2 | |- ( A e. ran B <-> E. x <. x , A >. e. B ) |