NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-fullfun Unicode version

Definition df-fullfun 5768
Description: Define the full function operator. This is a function over that agrees with the function value of at every point. (Contributed by SF, 9-Feb-2015.)
Assertion
Ref Expression
df-fullfun FullFun

Detailed syntax breakdown of Definition df-fullfun
StepHypRef Expression
1 cF . . 3
21cfullfun 5767 . 2 FullFun
3 cid 4763 . . . . 5
43, 1ccom 4721 . . . 4
53ccompl 3205 . . . . 5
65, 1ccom 4721 . . . 4
74, 6cdif 3206 . . 3
87cdm 4772 . . . . 5
98ccompl 3205 . . . 4
10 c0 3550 . . . . 5
1110csn 3737 . . . 4
129, 11cxp 4770 . . 3
137, 12cun 3207 . 2
142, 13wceq 1642 1 FullFun
Colors of variables: wff setvar class
This definition is referenced by:  fnfullfun  5858  fullfunexg  5859  fvfullfun  5864
  Copyright terms: Public domain W3C validator