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

Definition df-funs 5760
Description: Define the class of all functions. (Contributed by SF, 9-Feb-2015.)
Assertion
Ref Expression
df-funs Funs

Detailed syntax breakdown of Definition df-funs
StepHypRef Expression
1 cfuns 5759 . 2 Funs
2 vf . . . . 5
32cv 1641 . . . 4
43wfun 4775 . . 3
54, 2cab 2339 . 2
61, 5wceq 1642 1 Funs
Colors of variables: wff setvar class
This definition is referenced by:  funsex  5828  elfuns  5829  pmex  6005
  Copyright terms: Public domain W3C validator