Definition df-funs 5760

Description: Define the class of all functions. (Contributed by SF, 9-Feb-2015.)

Assertion

Ref	Expression
df-funs	⊢ Funs = {f ∣ Fun f}

Detailed syntax breakdown of Definition df-funs

Step	Hyp	Ref	Expression
1		cfuns 5759	. 2 class Funs
2		vf	. . . . 5 setvar f
3	2	cv 1641	. . . 4 class f
4	3	wfun 4775	. . 3 wff Fun f
5	4, 2	cab 2339	. 2 class {f ∣ Fun f}
6	1, 5	wceq 1642	1 wff Funs = {f ∣ Fun f}

This definition is referenced by:  funsex  5828  elfuns  5829  pmex  6005