Detailed syntax breakdown of Definition df-usgr
Step | Hyp | Ref
| Expression |
1 | | cusgr 27240 |
. 2
class
USGraph |
2 | | ve |
. . . . . . . 8
setvar 𝑒 |
3 | 2 | cv 1542 |
. . . . . . 7
class 𝑒 |
4 | 3 | cdm 5551 |
. . . . . 6
class dom 𝑒 |
5 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
6 | 5 | cv 1542 |
. . . . . . . . 9
class 𝑥 |
7 | | chash 13896 |
. . . . . . . . 9
class
♯ |
8 | 6, 7 | cfv 6380 |
. . . . . . . 8
class
(♯‘𝑥) |
9 | | c2 11885 |
. . . . . . . 8
class
2 |
10 | 8, 9 | wceq 1543 |
. . . . . . 7
wff
(♯‘𝑥) =
2 |
11 | | vv |
. . . . . . . . . 10
setvar 𝑣 |
12 | 11 | cv 1542 |
. . . . . . . . 9
class 𝑣 |
13 | 12 | cpw 4513 |
. . . . . . . 8
class 𝒫
𝑣 |
14 | | c0 4237 |
. . . . . . . . 9
class
∅ |
15 | 14 | csn 4541 |
. . . . . . . 8
class
{∅} |
16 | 13, 15 | cdif 3863 |
. . . . . . 7
class
(𝒫 𝑣 ∖
{∅}) |
17 | 10, 5, 16 | crab 3065 |
. . . . . 6
class {𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) =
2} |
18 | 4, 17, 3 | wf1 6377 |
. . . . 5
wff 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) =
2} |
19 | | vg |
. . . . . . 7
setvar 𝑔 |
20 | 19 | cv 1542 |
. . . . . 6
class 𝑔 |
21 | | ciedg 27088 |
. . . . . 6
class
iEdg |
22 | 20, 21 | cfv 6380 |
. . . . 5
class
(iEdg‘𝑔) |
23 | 18, 2, 22 | wsbc 3694 |
. . . 4
wff
[(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) =
2} |
24 | | cvtx 27087 |
. . . . 5
class
Vtx |
25 | 20, 24 | cfv 6380 |
. . . 4
class
(Vtx‘𝑔) |
26 | 23, 11, 25 | wsbc 3694 |
. . 3
wff
[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) =
2} |
27 | 26, 19 | cab 2714 |
. 2
class {𝑔 ∣
[(Vtx‘𝑔) /
𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) =
2}} |
28 | 1, 27 | wceq 1543 |
1
wff USGraph =
{𝑔 ∣
[(Vtx‘𝑔) /
𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) =
2}} |