Step | Hyp | Ref
| Expression |
1 | | cfdiv 47223 |
. 2
class
/f |
2 | | vf |
. . 3
setvar 𝑓 |
3 | | vg |
. . 3
setvar 𝑔 |
4 | | cvv 3475 |
. . 3
class
V |
5 | 2 | cv 1541 |
. . . . 5
class 𝑓 |
6 | 3 | cv 1541 |
. . . . 5
class 𝑔 |
7 | | cdiv 11871 |
. . . . . 6
class
/ |
8 | 7 | cof 7668 |
. . . . 5
class
∘f / |
9 | 5, 6, 8 | co 7409 |
. . . 4
class (𝑓 ∘f / 𝑔) |
10 | | cc0 11110 |
. . . . 5
class
0 |
11 | | csupp 8146 |
. . . . 5
class
supp |
12 | 6, 10, 11 | co 7409 |
. . . 4
class (𝑔 supp 0) |
13 | 9, 12 | cres 5679 |
. . 3
class ((𝑓 ∘f / 𝑔) ↾ (𝑔 supp 0)) |
14 | 2, 3, 4, 4, 13 | cmpo 7411 |
. 2
class (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓 ∘f / 𝑔) ↾ (𝑔 supp 0))) |
15 | 1, 14 | wceq 1542 |
1
wff
/f = (𝑓 ∈
V, 𝑔 ∈ V ↦
((𝑓 ∘f /
𝑔) ↾ (𝑔 supp 0))) |