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	|- ( ( Fun ( G \ { (/) } ) /\ { ( Base ` ndx ) , ( .ef ` ndx ) } C_ dom G ) -> ( iEdg ` G ) = ( .ef ` G ) )

Proof

Step	Hyp	Ref	Expression
1		basendxnedgfndx	|- ( Base ` ndx ) =/= ( .ef ` ndx )
2		fvex	|- ( Base ` ndx ) e. _V
3		fvex	|- ( .ef ` ndx ) e. _V
4	2 3	funiedgdm2val	|- ( ( Fun ( G \ { (/) } ) /\ ( Base ` ndx ) =/= ( .ef ` ndx ) /\ { ( Base ` ndx ) , ( .ef ` ndx ) } C_ dom G ) -> ( iEdg ` G ) = ( .ef ` G ) )
5	1 4	mp3an2	|- ( ( Fun ( G \ { (/) } ) /\ { ( Base ` ndx ) , ( .ef ` ndx ) } C_ dom G ) -> ( iEdg ` G ) = ( .ef ` G ) )