Detailed syntax breakdown of Definition df-vrgp
Step | Hyp | Ref
| Expression |
1 | | cvrgp 19098 |
. 2
class
varFGrp |
2 | | vi |
. . 3
setvar 𝑖 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vj |
. . . 4
setvar 𝑗 |
5 | 2 | cv 1542 |
. . . 4
class 𝑖 |
6 | 4 | cv 1542 |
. . . . . . 7
class 𝑗 |
7 | | c0 4237 |
. . . . . . 7
class
∅ |
8 | 6, 7 | cop 4547 |
. . . . . 6
class
〈𝑗,
∅〉 |
9 | 8 | cs1 14152 |
. . . . 5
class
〈“〈𝑗, ∅〉”〉 |
10 | | cefg 19096 |
. . . . . 6
class
~FG |
11 | 5, 10 | cfv 6380 |
. . . . 5
class (
~FG ‘𝑖) |
12 | 9, 11 | cec 8389 |
. . . 4
class
[〈“〈𝑗, ∅〉”〉](
~FG ‘𝑖) |
13 | 4, 5, 12 | cmpt 5135 |
. . 3
class (𝑗 ∈ 𝑖 ↦ [〈“〈𝑗, ∅〉”〉](
~FG ‘𝑖)) |
14 | 2, 3, 13 | cmpt 5135 |
. 2
class (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [〈“〈𝑗, ∅〉”〉](
~FG ‘𝑖))) |
15 | 1, 14 | wceq 1543 |
1
wff
varFGrp = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [〈“〈𝑗, ∅〉”〉](
~FG ‘𝑖))) |