Detailed syntax breakdown of Definition df-uncf
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cuncf 18257 | . 2
class 
uncurryF | 
| 2 |  | vc | . . 3
setvar 𝑐 | 
| 3 |  | vf | . . 3
setvar 𝑓 | 
| 4 |  | cvv 3479 | . . 3
class
V | 
| 5 |  | c1 11157 | . . . . . 6
class
1 | 
| 6 | 2 | cv 1538 | . . . . . 6
class 𝑐 | 
| 7 | 5, 6 | cfv 6560 | . . . . 5
class (𝑐‘1) | 
| 8 |  | c2 12322 | . . . . . 6
class
2 | 
| 9 | 8, 6 | cfv 6560 | . . . . 5
class (𝑐‘2) | 
| 10 |  | cevlf 18255 | . . . . 5
class 
evalF | 
| 11 | 7, 9, 10 | co 7432 | . . . 4
class ((𝑐‘1)
evalF (𝑐‘2)) | 
| 12 | 3 | cv 1538 | . . . . . 6
class 𝑓 | 
| 13 |  | cc0 11156 | . . . . . . . 8
class
0 | 
| 14 | 13, 6 | cfv 6560 | . . . . . . 7
class (𝑐‘0) | 
| 15 |  | c1stf 18215 | . . . . . . 7
class 
1stF | 
| 16 | 14, 7, 15 | co 7432 | . . . . . 6
class ((𝑐‘0)
1stF (𝑐‘1)) | 
| 17 |  | ccofu 17902 | . . . . . 6
class 
∘func | 
| 18 | 12, 16, 17 | co 7432 | . . . . 5
class (𝑓 ∘func
((𝑐‘0)
1stF (𝑐‘1))) | 
| 19 |  | c2ndf 18216 | . . . . . 6
class 
2ndF | 
| 20 | 14, 7, 19 | co 7432 | . . . . 5
class ((𝑐‘0)
2ndF (𝑐‘1)) | 
| 21 |  | cprf 18217 | . . . . 5
class 
〈,〉F | 
| 22 | 18, 20, 21 | co 7432 | . . . 4
class ((𝑓 ∘func
((𝑐‘0)
1stF (𝑐‘1))) 〈,〉F
((𝑐‘0)
2ndF (𝑐‘1))) | 
| 23 | 11, 22, 17 | co 7432 | . . 3
class (((𝑐‘1)
evalF (𝑐‘2)) ∘func
((𝑓
∘func ((𝑐‘0) 1stF
(𝑐‘1)))
〈,〉F ((𝑐‘0) 2ndF
(𝑐‘1)))) | 
| 24 | 2, 3, 4, 4, 23 | cmpo 7434 | . 2
class (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2))
∘func ((𝑓 ∘func ((𝑐‘0)
1stF (𝑐‘1))) 〈,〉F
((𝑐‘0)
2ndF (𝑐‘1))))) | 
| 25 | 1, 24 | wceq 1539 | 1
wff 
uncurryF = (𝑐 ∈ V, 𝑓 ∈ V ↦ (((𝑐‘1) evalF (𝑐‘2))
∘func ((𝑓 ∘func ((𝑐‘0)
1stF (𝑐‘1))) 〈,〉F
((𝑐‘0)
2ndF (𝑐‘1))))) |