Definition df-fullfun 31982

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

Assertion

Ref	Expression
df-fullfun	|- FullFun F = (Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) )

Detailed syntax breakdown of Definition df-fullfun

Step	Hyp	Ref	Expression
1		cF	. . 3 class F
2	1	cfullfn 31957	. 2 class FullFun F
3	1	cfunpart 31956	. . 3 class Funpart F
4		cvv 3200	. . . . 5 class _V
5	3	cdm 5114	. . . . 5 class dom Funpart F
6	4, 5	cdif 3571	. . . 4 class ( _V \ dom Funpart F )
7		c0 3915	. . . . 5 class (/)
8	7	csn 4177	. . . 4 class { (/) }
9	6, 8	cxp 5112	. . 3 class ( ( _V \ dom Funpart F ) X. { (/) } )
10	3, 9	cun 3572	. 2 class (Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) )
11	2, 10	wceq 1483	1 wff FullFun F = (Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) )

This definition is referenced by:  fullfunfnv  32053  fullfunfv  32054