Definition df-fullfun

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	|- F
1	0	cfullfn	|- FullFun F
2	0	cfunpart	|- Funpart F
3		cvv	|- _V
4	2	cdm	|- dom Funpart F
5	3 4	cdif	|- ( _V \ dom Funpart F )
6		c0	|- (/)
7	6	csn	|- { (/) }
8	5 7	cxp	|- ( ( _V \ dom Funpart F ) X. { (/) } )
9	2 8	cun	|- ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) )
10	1 9	wceq	|- FullFun F = ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) )