Definition df-funs 25705

Description: Define the class of all functions. See elfuns 25760 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 25681	. 2 class Funs
2		cvv 2956	. . . . 5 class _V
3	2, 2	cxp 4876	. . . 4 class ( _V X. _V )
4	3	cpw 3799	. . 3 class ~P ( _V X. _V )
5		cep 4492	. . . . 5 class _E
6		c1st 6347	. . . . . . 7 class 1st
7		cid 4493	. . . . . . . . 9 class _I
8	2, 7	cdif 3317	. . . . . . . 8 class ( _V \ _I )
9		c2nd 6348	. . . . . . . 8 class 2nd
10	8, 9	ccom 4882	. . . . . . 7 class ( ( _V \ _I ) o. 2nd )
11	6, 10	ctxp 25674	. . . . . 6 class ( 1st (x) ( ( _V \ _I ) o. 2nd ) )
12	5	ccnv 4877	. . . . . 6 class `' _E
13	11, 12	ccom 4882	. . . . 5 class ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E )
14	5, 13	ccom 4882	. . . 4 class ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) )
15	14	cfix 25679	. . 3 class Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) )
16	4, 15	cdif 3317	. 2 class ( ~P ( _V X. _V ) \ Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) )
17	1, 16	wceq 1652	1 wff Funs = ( ~P ( _V X. _V ) \ Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) )

This definition is referenced by:  elfuns  25760