# Metamath Proof Explorer

## Theorem funiedgval

Description: The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 21-Sep-2020) (Revised by AV, 7-Jun-2021) (Revised by AV, 12-Nov-2021)

Ref Expression
Assertion funiedgval ${⊢}\left(\mathrm{Fun}\left({G}\setminus \left\{\varnothing \right\}\right)\wedge \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}\subseteq \mathrm{dom}{G}\right)\to \mathrm{iEdg}\left({G}\right)=\mathrm{ef}\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 slotsbaseefdif ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{ef}\left(\mathrm{ndx}\right)$
2 fvex ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$
3 fvex ${⊢}\mathrm{ef}\left(\mathrm{ndx}\right)\in \mathrm{V}$
4 2 3 funiedgdm2val ${⊢}\left(\mathrm{Fun}\left({G}\setminus \left\{\varnothing \right\}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{ef}\left(\mathrm{ndx}\right)\wedge \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}\subseteq \mathrm{dom}{G}\right)\to \mathrm{iEdg}\left({G}\right)=\mathrm{ef}\left({G}\right)$
5 1 4 mp3an2 ${⊢}\left(\mathrm{Fun}\left({G}\setminus \left\{\varnothing \right\}\right)\wedge \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}\subseteq \mathrm{dom}{G}\right)\to \mathrm{iEdg}\left({G}\right)=\mathrm{ef}\left({G}\right)$