# Metamath Proof Explorer

Description: An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017) (Revised by AV, 18-Jan-2020)

Ref Expression
Hypotheses uhgrf.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
uhgrf.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
Assertion uhgrss ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {F}\in \mathrm{dom}{E}\right)\to {E}\left({F}\right)\subseteq {V}$

### Proof

Step Hyp Ref Expression
1 uhgrf.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 uhgrf.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
3 1 2 uhgrf ${⊢}{G}\in \mathrm{UHGraph}\to {E}:\mathrm{dom}{E}⟶𝒫{V}\setminus \left\{\varnothing \right\}$
4 3 ffvelrnda ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {F}\in \mathrm{dom}{E}\right)\to {E}\left({F}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)$
5 4 eldifad ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {F}\in \mathrm{dom}{E}\right)\to {E}\left({F}\right)\in 𝒫{V}$
6 5 elpwid ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {F}\in \mathrm{dom}{E}\right)\to {E}\left({F}\right)\subseteq {V}$