Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-comf Structured version   Unicode version

Definition df-comf 13888
 Description: Define the functionalized composition operator, which is exactly like comp but is guaranteed to be a function of the proper type. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
df-comf compf comp
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-comf
StepHypRef Expression
1 ccomf 13884 . 2 compf
2 vc . . 3
3 cvv 2948 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1651 . . . . . 6
7 cbs 13461 . . . . . 6
86, 7cfv 5446 . . . . 5
98, 8cxp 4868 . . . 4
10 vg . . . . 5
11 vf . . . . 5
124cv 1651 . . . . . . 7
13 c2nd 6340 . . . . . . 7
1412, 13cfv 5446 . . . . . 6
155cv 1651 . . . . . 6
16 chom 13532 . . . . . . 7
176, 16cfv 5446 . . . . . 6
1814, 15, 17co 6073 . . . . 5
1912, 17cfv 5446 . . . . 5
2010cv 1651 . . . . . 6
2111cv 1651 . . . . . 6
22 cco 13533 . . . . . . . 8 comp
236, 22cfv 5446 . . . . . . 7 comp
2412, 15, 23co 6073 . . . . . 6 comp
2520, 21, 24co 6073 . . . . 5 comp
2610, 11, 18, 19, 25cmpt2 6075 . . . 4 comp
274, 5, 9, 8, 26cmpt2 6075 . . 3 comp
282, 3, 27cmpt 4258 . 2 comp
291, 28wceq 1652 1 compf comp
 Colors of variables: wff set class This definition is referenced by:  comfffval  13916
 Copyright terms: Public domain W3C validator