Metamath Proof Explorer


Theorem funiedgdm2val

Description: The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020) (Revised by AV, 7-Jun-2021) (Revised by AV, 12-Nov-2021)

Ref Expression
Hypotheses funvtxdm2val.a A V
funvtxdm2val.b B V
Assertion funiedgdm2val Fun G A B A B dom G iEdg G = ef G

Proof

Step Hyp Ref Expression
1 funvtxdm2val.a A V
2 funvtxdm2val.b B V
3 iedgval iEdg G = if G V × V 2 nd G ef G
4 1 2 fun2dmnop0 Fun G A B A B dom G ¬ G V × V
5 4 iffalsed Fun G A B A B dom G if G V × V 2 nd G ef G = ef G
6 3 5 syl5eq Fun G A B A B dom G iEdg G = ef G