# Metamath Proof Explorer

## Theorem usgrf

Description: The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 13-Oct-2020)

Ref Expression
Hypotheses isuspgr.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
isuspgr.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
Assertion usgrf ${⊢}{G}\in \mathrm{USGraph}\to {E}:\mathrm{dom}{E}\underset{1-1}{⟶}\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|=2\right\}$

### Proof

Step Hyp Ref Expression
1 isuspgr.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 isuspgr.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
3 1 2 isusgr ${⊢}{G}\in \mathrm{USGraph}\to \left({G}\in \mathrm{USGraph}↔{E}:\mathrm{dom}{E}\underset{1-1}{⟶}\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|=2\right\}\right)$
4 3 ibi ${⊢}{G}\in \mathrm{USGraph}\to {E}:\mathrm{dom}{E}\underset{1-1}{⟶}\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|=2\right\}$