Description: The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by AV, 18-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | usgrf1oedg.i | |
|
usgrf1oedg.e | |
||
Assertion | usgrf1oedg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | usgrf1oedg.i | |
|
2 | usgrf1oedg.e | |
|
3 | eqid | |
|
4 | 3 1 | usgrf | |
5 | f1f1orn | |
|
6 | 4 5 | syl | |
7 | edgval | |
|
8 | 7 | a1i | |
9 | 1 | eqcomi | |
10 | 9 | rneqi | |
11 | 8 10 | eqtrdi | |
12 | 2 11 | eqtrid | |
13 | 12 | f1oeq3d | |
14 | 6 13 | mpbird | |