Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fullfun Unicode version

Definition df-fullfun 24416
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.)
Assertion
Ref Expression
df-fullfun  |- FullFun F  =  (Funpart F  u.  (
( _V  \  dom Funpart F )  X.  { (/) } ) )

Detailed syntax breakdown of Definition df-fullfun
StepHypRef Expression
1 cF . . 3  class  F
21cfullfn 24393 . 2  class FullFun F
31cfunpart 24392 . . 3  class Funpart F
4 cvv 2788 . . . . 5  class  _V
53cdm 4689 . . . . 5  class  dom Funpart F
64, 5cdif 3149 . . . 4  class  ( _V 
\  dom Funpart F )
7 c0 3455 . . . . 5  class  (/)
87csn 3640 . . . 4  class  { (/) }
96, 8cxp 4687 . . 3  class  ( ( _V  \  dom Funpart F )  X.  { (/) } )
103, 9cun 3150 . 2  class  (Funpart F  u.  ( ( _V  \  dom Funpart F )  X.  { (/)
} ) )
112, 10wceq 1623 1  wff FullFun F  =  (Funpart F  u.  (
( _V  \  dom Funpart F )  X.  { (/) } ) )
Colors of variables: wff set class
This definition is referenced by:  fullfunfnv  24484  fullfunfv  24485
  Copyright terms: Public domain W3C validator