Detailed syntax breakdown of Definition df-ablo
Step | Hyp | Ref
| Expression |
1 | | cablo 28625 |
. 2
class
AbelOp |
2 | | vx |
. . . . . . . 8
setvar 𝑥 |
3 | 2 | cv 1542 |
. . . . . . 7
class 𝑥 |
4 | | vy |
. . . . . . . 8
setvar 𝑦 |
5 | 4 | cv 1542 |
. . . . . . 7
class 𝑦 |
6 | | vg |
. . . . . . . 8
setvar 𝑔 |
7 | 6 | cv 1542 |
. . . . . . 7
class 𝑔 |
8 | 3, 5, 7 | co 7213 |
. . . . . 6
class (𝑥𝑔𝑦) |
9 | 5, 3, 7 | co 7213 |
. . . . . 6
class (𝑦𝑔𝑥) |
10 | 8, 9 | wceq 1543 |
. . . . 5
wff (𝑥𝑔𝑦) = (𝑦𝑔𝑥) |
11 | 7 | crn 5552 |
. . . . 5
class ran 𝑔 |
12 | 10, 4, 11 | wral 3061 |
. . . 4
wff
∀𝑦 ∈ ran
𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥) |
13 | 12, 2, 11 | wral 3061 |
. . 3
wff
∀𝑥 ∈ ran
𝑔∀𝑦 ∈ ran 𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥) |
14 | | cgr 28570 |
. . 3
class
GrpOp |
15 | 13, 6, 14 | crab 3065 |
. 2
class {𝑔 ∈ GrpOp ∣
∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥)} |
16 | 1, 15 | wceq 1543 |
1
wff AbelOp =
{𝑔 ∈ GrpOp ∣
∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥)} |