Detailed syntax breakdown of Definition df-uhgr
Step | Hyp | Ref
| Expression |
1 | | cuhgr 27422 |
. 2
class
UHGraph |
2 | | ve |
. . . . . . . 8
setvar 𝑒 |
3 | 2 | cv 1541 |
. . . . . . 7
class 𝑒 |
4 | 3 | cdm 5589 |
. . . . . 6
class dom 𝑒 |
5 | | vv |
. . . . . . . . 9
setvar 𝑣 |
6 | 5 | cv 1541 |
. . . . . . . 8
class 𝑣 |
7 | 6 | cpw 4539 |
. . . . . . 7
class 𝒫
𝑣 |
8 | | c0 4262 |
. . . . . . . 8
class
∅ |
9 | 8 | csn 4567 |
. . . . . . 7
class
{∅} |
10 | 7, 9 | cdif 3889 |
. . . . . 6
class
(𝒫 𝑣 ∖
{∅}) |
11 | 4, 10, 3 | wf 6427 |
. . . . 5
wff 𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅}) |
12 | | vg |
. . . . . . 7
setvar 𝑔 |
13 | 12 | cv 1541 |
. . . . . 6
class 𝑔 |
14 | | ciedg 27363 |
. . . . . 6
class
iEdg |
15 | 13, 14 | cfv 6431 |
. . . . 5
class
(iEdg‘𝑔) |
16 | 11, 2, 15 | wsbc 3720 |
. . . 4
wff
[(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅}) |
17 | | cvtx 27362 |
. . . . 5
class
Vtx |
18 | 13, 17 | cfv 6431 |
. . . 4
class
(Vtx‘𝑔) |
19 | 16, 5, 18 | wsbc 3720 |
. . 3
wff
[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅}) |
20 | 19, 12 | cab 2717 |
. 2
class {𝑔 ∣
[(Vtx‘𝑔) /
𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})} |
21 | 1, 20 | wceq 1542 |
1
wff UHGraph =
{𝑔 ∣
[(Vtx‘𝑔) /
𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})} |