# Metamath Proof Explorer

## Theorem usgredg2vtxeu

Description: For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020) (Proof shortened by AV, 6-Dec-2020)

Ref Expression
Assertion usgredg2vtxeu ${⊢}\left({G}\in \mathrm{USGraph}\wedge {E}\in \mathrm{Edg}\left({G}\right)\wedge {Y}\in {E}\right)\to \exists !{y}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}{E}=\left\{{Y},{y}\right\}$

### Proof

Step Hyp Ref Expression
1 usgruspgr ${⊢}{G}\in \mathrm{USGraph}\to {G}\in \mathrm{USHGraph}$
2 uspgredg2vtxeu ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {E}\in \mathrm{Edg}\left({G}\right)\wedge {Y}\in {E}\right)\to \exists !{y}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}{E}=\left\{{Y},{y}\right\}$
3 1 2 syl3an1 ${⊢}\left({G}\in \mathrm{USGraph}\wedge {E}\in \mathrm{Edg}\left({G}\right)\wedge {Y}\in {E}\right)\to \exists !{y}\in \mathrm{Vtx}\left({G}\right)\phantom{\rule{.4em}{0ex}}{E}=\left\{{Y},{y}\right\}$