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

Definition df-funs 25624
Description: Define the class of all functions. See elfuns 25676 for membership. (Contributed by Scott Fenton, 18-Feb-2013.)
Assertion
Ref Expression
df-funs  |-  Funs  =  ( ~P ( _V  X.  _V )  \  Fix (  _E  o.  ( ( 1st  (x)  ( ( _V  \  _I  )  o.  2nd ) )  o.  `'  _E  ) ) )

Detailed syntax breakdown of Definition df-funs
StepHypRef Expression
1 cfuns 25602 . 2  class  Funs
2 cvv 2924 . . . . 5  class  _V
32, 2cxp 4843 . . . 4  class  ( _V 
X.  _V )
43cpw 3767 . . 3  class  ~P ( _V  X.  _V )
5 cep 4460 . . . . 5  class  _E
6 c1st 6314 . . . . . . 7  class  1st
7 cid 4461 . . . . . . . . 9  class  _I
82, 7cdif 3285 . . . . . . . 8  class  ( _V 
\  _I  )
9 c2nd 6315 . . . . . . . 8  class  2nd
108, 9ccom 4849 . . . . . . 7  class  ( ( _V  \  _I  )  o.  2nd )
116, 10ctxp 25595 . . . . . 6  class  ( 1st  (x)  ( ( _V  \  _I  )  o.  2nd ) )
125ccnv 4844 . . . . . 6  class  `'  _E
1311, 12ccom 4849 . . . . 5  class  ( ( 1st  (x)  ( ( _V  \  _I  )  o. 
2nd ) )  o.  `'  _E  )
145, 13ccom 4849 . . . 4  class  (  _E  o.  ( ( 1st  (x)  ( ( _V  \  _I  )  o.  2nd ) )  o.  `'  _E  ) )
1514cfix 25600 . . 3  class  Fix (  _E  o.  ( ( 1st  (x)  ( ( _V  \  _I  )  o.  2nd ) )  o.  `'  _E  ) )
164, 15cdif 3285 . 2  class  ( ~P ( _V  X.  _V )  \  Fix (  _E  o.  ( ( 1st  (x)  ( ( _V  \  _I  )  o.  2nd ) )  o.  `'  _E  ) ) )
171, 16wceq 1649 1  wff  Funs  =  ( ~P ( _V  X.  _V )  \  Fix (  _E  o.  ( ( 1st  (x)  ( ( _V  \  _I  )  o.  2nd ) )  o.  `'  _E  ) ) )
Colors of variables: wff set class
This definition is referenced by:  elfuns  25676
  Copyright terms: Public domain W3C validator