Description: Alternate definition of range. (Contributed by Peter Mazsa, 1-Aug-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | dfrn6 | |- ran R = { x | [ x ] `' R =/= (/) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rn | |- ran R = dom `' R |
|
2 | dfdm6 | |- dom `' R = { x | [ x ] `' R =/= (/) } |
|
3 | 1 2 | eqtri | |- ran R = { x | [ x ] `' R =/= (/) } |