Metamath Proof Explorer


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 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ×

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF class F
1 0 cfullfn class 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F
2 0 cfunpart class 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
3 cvv class V
4 2 cdm class dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
5 3 4 cdif class V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
6 c0 class
7 6 csn class
8 5 7 cxp class V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ×
9 2 8 cun class 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ×
10 1 9 wceq wff 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ×