Metamath Proof Explorer
Description: Define the range function. See brrange for its value. (Contributed by Scott Fenton, 11-Apr-2014)
|
|
Ref |
Expression |
|
Assertion |
df-range |
⊢ Range = Image ( 2nd ↾ ( V × V ) ) |
Detailed syntax breakdown
| Step |
Hyp |
Ref |
Expression |
| 0 |
|
crange |
⊢ Range |
| 1 |
|
c2nd |
⊢ 2nd |
| 2 |
|
cvv |
⊢ V |
| 3 |
2 2
|
cxp |
⊢ ( V × V ) |
| 4 |
1 3
|
cres |
⊢ ( 2nd ↾ ( V × V ) ) |
| 5 |
4
|
cimage |
⊢ Image ( 2nd ↾ ( V × V ) ) |
| 6 |
0 5
|
wceq |
⊢ Range = Image ( 2nd ↾ ( V × V ) ) |