Detailed syntax breakdown of Definition df-fdiv
Step | Hyp | Ref
| Expression |
1 | | cfdiv 43360 |
. 2
class
/f |
2 | | vf |
. . 3
setvar 𝑓 |
3 | | vg |
. . 3
setvar 𝑔 |
4 | | cvv 3398 |
. . 3
class
V |
5 | 2 | cv 1600 |
. . . . 5
class 𝑓 |
6 | 3 | cv 1600 |
. . . . 5
class 𝑔 |
7 | | cdiv 11035 |
. . . . . 6
class
/ |
8 | 7 | cof 7174 |
. . . . 5
class
∘𝑓 / |
9 | 5, 6, 8 | co 6924 |
. . . 4
class (𝑓 ∘𝑓 /
𝑔) |
10 | | cc0 10274 |
. . . . 5
class
0 |
11 | | csupp 7578 |
. . . . 5
class
supp |
12 | 6, 10, 11 | co 6924 |
. . . 4
class (𝑔 supp 0) |
13 | 9, 12 | cres 5359 |
. . 3
class ((𝑓 ∘𝑓 /
𝑔) ↾ (𝑔 supp 0)) |
14 | 2, 3, 4, 4, 13 | cmpt2 6926 |
. 2
class (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓 ∘𝑓 / 𝑔) ↾ (𝑔 supp 0))) |
15 | 1, 14 | wceq 1601 |
1
wff
/f = (𝑓 ∈
V, 𝑔 ∈ V ↦
((𝑓
∘𝑓 / 𝑔) ↾ (𝑔 supp 0))) |