New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-ranfn | Unicode version |
Description: Define the range function. This is a function wrapper for the range operator. (Contributed by Scott Fenton, 9-Aug-2019.) |
Ref | Expression |
---|---|
df-ranfn | Ran |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cranfn 5771 | . 2 Ran | |
2 | vx | . . 3 | |
3 | cvv 2859 | . . 3 | |
4 | 2 | cv 1641 | . . . 4 |
5 | 4 | crn 4773 | . . 3 |
6 | 2, 3, 5 | cmpt 5651 | . 2 |
7 | 1, 6 | wceq 1642 | 1 Ran |
Colors of variables: wff setvar class |
This definition is referenced by: fvranfn 5869 ranfnex 5871 |
Copyright terms: Public domain | W3C validator |