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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cF | ||
1 | 0 | cfullfn | |
2 | 0 | cfunpart | |
3 | cvv | ||
4 | 2 | cdm | |
5 | 3 4 | cdif | |
6 | c0 | ||
7 | 6 | csn | |
8 | 5 7 | cxp | |
9 | 2 8 | cun | |
10 | 1 9 | wceq |