Definition df-ranfn 5773

Description: Define the range function. This is a function wrapper for the range operator. (Contributed by Scott Fenton, 9-Aug-2019.)

Assertion

Ref	Expression
df-ranfn	|- Ran = (x e. _V |-> ran x)

Detailed syntax breakdown of Definition df-ranfn

Step	Hyp	Ref	Expression
1		cranfn 5772	. 2 class Ran
2		vx	. . 3 setvar x
3		cvv 2860	. . 3 class _V
4	2	cv 1641	. . . 4 class x
5	4	crn 4774	. . 3 class ran x
6	2, 3, 5	cmpt 5652	. 2 class (x e. _V |-> ran x)
7	1, 6	wceq 1642	1 wff Ran = (x e. _V |-> ran x)

This definition is referenced by:  fvranfn  5870  ranfnex  5872