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

Step	Hyp	Ref	Expression
1		cfuns 25602	. 2 class Funs
2		cvv 2924	. . . . 5 class _V
3	2, 2	cxp 4843	. . . 4 class ( _V X. _V )
4	3	cpw 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
8	2, 7	cdif 3285	. . . . . . . 8 class ( _V \ _I )
9		c2nd 6315	. . . . . . . 8 class 2nd
10	8, 9	ccom 4849	. . . . . . 7 class ( ( _V \ _I ) o. 2nd )
11	6, 10	ctxp 25595	. . . . . 6 class ( 1st (x) ( ( _V \ _I ) o. 2nd ) )
12	5	ccnv 4844	. . . . . 6 class `' _E
13	11, 12	ccom 4849	. . . . 5 class ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E )
14	5, 13	ccom 4849	. . . 4 class ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) )
15	14	cfix 25600	. . 3 class Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) )
16	4, 15	cdif 3285	. 2 class ( ~P ( _V X. _V ) \ Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) )
17	1, 16	wceq 1649	1 wff Funs = ( ~P ( _V X. _V ) \ Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) )

This definition is referenced by:  elfuns  25676