Description: In a simple graph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 18-Oct-2020) (Proof shortened by AV, 11-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ushgredgedg.e | |
|
ushgredgedg.i | |
||
ushgredgedg.v | |
||
ushgredgedg.a | |
||
ushgredgedg.b | |
||
ushgredgedg.f | |
||
Assertion | usgredgedg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ushgredgedg.e | |
|
2 | ushgredgedg.i | |
|
3 | ushgredgedg.v | |
|
4 | ushgredgedg.a | |
|
5 | ushgredgedg.b | |
|
6 | ushgredgedg.f | |
|
7 | usgruspgr | |
|
8 | uspgrushgr | |
|
9 | 7 8 | syl | |
10 | 1 2 3 4 5 6 | ushgredgedg | |
11 | 9 10 | sylan | |