Detailed syntax breakdown of Definition df-ass
Step | Hyp | Ref
| Expression |
1 | | cass 35623 |
. 2
class
Ass |
2 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
3 | 2 | cv 1541 |
. . . . . . . . 9
class 𝑥 |
4 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
5 | 4 | cv 1541 |
. . . . . . . . 9
class 𝑦 |
6 | | vg |
. . . . . . . . . 10
setvar 𝑔 |
7 | 6 | cv 1541 |
. . . . . . . . 9
class 𝑔 |
8 | 3, 5, 7 | co 7170 |
. . . . . . . 8
class (𝑥𝑔𝑦) |
9 | | vz |
. . . . . . . . 9
setvar 𝑧 |
10 | 9 | cv 1541 |
. . . . . . . 8
class 𝑧 |
11 | 8, 10, 7 | co 7170 |
. . . . . . 7
class ((𝑥𝑔𝑦)𝑔𝑧) |
12 | 5, 10, 7 | co 7170 |
. . . . . . . 8
class (𝑦𝑔𝑧) |
13 | 3, 12, 7 | co 7170 |
. . . . . . 7
class (𝑥𝑔(𝑦𝑔𝑧)) |
14 | 11, 13 | wceq 1542 |
. . . . . 6
wff ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) |
15 | 7 | cdm 5525 |
. . . . . . 7
class dom 𝑔 |
16 | 15 | cdm 5525 |
. . . . . 6
class dom dom
𝑔 |
17 | 14, 9, 16 | wral 3053 |
. . . . 5
wff
∀𝑧 ∈ dom
dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) |
18 | 17, 4, 16 | wral 3053 |
. . . 4
wff
∀𝑦 ∈ dom
dom 𝑔∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) |
19 | 18, 2, 16 | wral 3053 |
. . 3
wff
∀𝑥 ∈ dom
dom 𝑔∀𝑦 ∈ dom dom 𝑔∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) |
20 | 19, 6 | cab 2716 |
. 2
class {𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))} |
21 | 1, 20 | wceq 1542 |
1
wff Ass =
{𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))} |