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	$$⊢\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}F=\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F\cup \left(\left(\mathrm{V}\setminus \mathrm{dom}\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F\right)\times \left\{\varnothing \right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1	0	cfullfn	$$class\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}F$$
2	0	cfunpart	$$class\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F$$
3		cvv	$$class\mathrm{V}$$
4	2	cdm	$$class\mathrm{dom}\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F$$
5	3 4	cdif	$$class\left(\mathrm{V}\setminus \mathrm{dom}\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F\right)$$
6		c0	$$class\varnothing$$
7	6	csn	$$class\left\{\varnothing \right\}$$
8	5 7	cxp	$$class\left(\left(\mathrm{V}\setminus \mathrm{dom}\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F\right)\times \left\{\varnothing \right\}\right)$$
9	2 8	cun	$$class\left(\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F\cup \left(\left(\mathrm{V}\setminus \mathrm{dom}\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F\right)\times \left\{\varnothing \right\}\right)\right)$$
10	1 9	wceq	$$wff\mathrm{𝖥𝗎𝗅𝗅𝖥𝗎𝗇}F=\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F\cup \left(\left(\mathrm{V}\setminus \mathrm{dom}\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F\right)\times \left\{\varnothing \right\}\right)$$