Definition df-domfn 5770

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

Assertion

Ref	Expression
df-domfn	⊢ Dom = (x ∈ V ↦ dom x)

Detailed syntax breakdown of Definition df-domfn

Step	Hyp	Ref	Expression
1		cdomfn 5769	. 2 class Dom
2		vx	. . 3 setvar x
3		cvv 2859	. . 3 class V
4	2	cv 1641	. . . 4 class x
5	4	cdm 4772	. . 3 class dom x
6	2, 3, 5	cmpt 5651	. 2 class (x ∈ V ↦ dom x)
7	1, 6	wceq 1642	1 wff Dom = (x ∈ V ↦ dom x)

This definition is referenced by:  fvdomfn  5868  domfnex  5870