Detailed syntax breakdown of Definition df-funpart
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cF | . . 3
class 𝐹 | 
| 2 | 1 | cfunpart 35851 | . 2
class
Funpart𝐹 | 
| 3 | 1 | cimage 35842 | . . . . . 6
class
Image𝐹 | 
| 4 |  | csingle 35840 | . . . . . 6
class
Singleton | 
| 5 | 3, 4 | ccom 5688 | . . . . 5
class
(Image𝐹 ∘
Singleton) | 
| 6 |  | cvv 3479 | . . . . . 6
class
V | 
| 7 |  | csingles 35841 | . . . . . 6
class  Singletons | 
| 8 | 6, 7 | cxp 5682 | . . . . 5
class (V
×  Singletons ) | 
| 9 | 5, 8 | cin 3949 | . . . 4
class
((Image𝐹 ∘
Singleton) ∩ (V ×  Singletons
)) | 
| 10 | 9 | cdm 5684 | . . 3
class dom
((Image𝐹 ∘ Singleton)
∩ (V ×  Singletons )) | 
| 11 | 1, 10 | cres 5686 | . 2
class (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
×  Singletons ))) | 
| 12 | 2, 11 | wceq 1539 | 1
wff
Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V
×  Singletons ))) |