Definition df-fullfun 35853

Description: Define the full function over 𝐹. This is a function with domain V that always agrees with 𝐹 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)

Assertion

Ref	Expression
df-fullfun	⊢ FullFun𝐹 = (Funpart𝐹 ∪ ((V ∖ dom Funpart𝐹) × {∅}))

Detailed syntax breakdown of Definition df-fullfun

Step	Hyp	Ref	Expression
1		cF	. . 3 class 𝐹
2	1	cfullfn 35828	. 2 class FullFun𝐹
3	1	cfunpart 35827	. . 3 class Funpart𝐹
4		cvv 3436	. . . . 5 class V
5	3	cdm 5619	. . . . 5 class dom Funpart𝐹
6	4, 5	cdif 3900	. . . 4 class (V ∖ dom Funpart𝐹)
7		c0 4284	. . . . 5 class ∅
8	7	csn 4577	. . . 4 class {∅}
9	6, 8	cxp 5617	. . 3 class ((V ∖ dom Funpart𝐹) × {∅})
10	3, 9	cun 3901	. 2 class (Funpart𝐹 ∪ ((V ∖ dom Funpart𝐹) × {∅}))
11	2, 10	wceq 1540	1 wff FullFun𝐹 = (Funpart𝐹 ∪ ((V ∖ dom Funpart𝐹) × {∅}))

This definition is referenced by:  fullfunfnv  35924  fullfunfv  35925