Definition df-funs 34864

Description: Define the class of all functions. See elfuns 34918 for membership. (Contributed by Scott Fenton, 18-Feb-2013.)

Assertion

Ref	Expression
df-funs	⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))

Detailed syntax breakdown of Definition df-funs

Step	Hyp	Ref	Expression
1		cfuns 34840	. 2 class Funs
2		cvv 3475	. . . . 5 class V
3	2, 2	cxp 5675	. . . 4 class (V × V)
4	3	cpw 4603	. . 3 class 𝒫 (V × V)
5		cep 5580	. . . . 5 class E
6		c1st 7973	. . . . . . 7 class 1st
7		cid 5574	. . . . . . . . 9 class I
8	2, 7	cdif 3946	. . . . . . . 8 class (V ∖ I )
9		c2nd 7974	. . . . . . . 8 class 2nd
10	8, 9	ccom 5681	. . . . . . 7 class ((V ∖ I ) ∘ 2nd )
11	6, 10	ctxp 34833	. . . . . 6 class (1st ⊗ ((V ∖ I ) ∘ 2nd ))
12	5	ccnv 5676	. . . . . 6 class ◡ E
13	11, 12	ccom 5681	. . . . 5 class ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )
14	5, 13	ccom 5681	. . . 4 class ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))
15	14	cfix 34838	. . 3 class Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))
16	4, 15	cdif 3946	. 2 class (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))
17	1, 16	wceq 1542	1 wff Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))

This definition is referenced by:  elfuns  34918