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

Definition df-fullfun 5768
 Description: Define the full function operator. This is a function over V that agrees with the function value of F at every point. (Contributed by SF, 9-Feb-2015.)
Assertion
Ref Expression
df-fullfun FullFun F = ((( I F) ( ∼ I F)) ∪ ( ∼ dom (( I F) ( ∼ I F)) × {}))

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