Definition df-funs 31968

Description: Define the class of all functions. See elfuns 32022 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 31944	. 2 class Funs
2		cvv 3200	. . . . 5 class _V
3	2, 2	cxp 5112	. . . 4 class ( _V X. _V )
4	3	cpw 4158	. . 3 class ~P ( _V X. _V )
5		cep 5028	. . . . 5 class _E
6		c1st 7166	. . . . . . 7 class 1st
7		cid 5023	. . . . . . . . 9 class _I
8	2, 7	cdif 3571	. . . . . . . 8 class ( _V \ _I )
9		c2nd 7167	. . . . . . . 8 class 2nd
10	8, 9	ccom 5118	. . . . . . 7 class ( ( _V \ _I ) o. 2nd )
11	6, 10	ctxp 31937	. . . . . 6 class ( 1st (x) ( ( _V \ _I ) o. 2nd ) )
12	5	ccnv 5113	. . . . . 6 class `' _E
13	11, 12	ccom 5118	. . . . 5 class ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E )
14	5, 13	ccom 5118	. . . 4 class ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) )
15	14	cfix 31942	. . 3 class Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) )
16	4, 15	cdif 3571	. 2 class ( ~P ( _V X. _V ) \ Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) )
17	1, 16	wceq 1483	1 wff Funs = ( ~P ( _V X. _V ) \ Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) )

This definition is referenced by:  elfuns  32022