Metamath Proof Explorer


Theorem umgr2v2eedg

Description: The set of edges in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020)

Ref Expression
Hypothesis umgr2v2evtx.g G = V 0 A B 1 A B
Assertion umgr2v2eedg V W A V B V Edg G = A B

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g G = V 0 A B 1 A B
2 edgval Edg G = ran iEdg G
3 2 a1i V W A V B V Edg G = ran iEdg G
4 1 umgr2v2eiedg V W A V B V iEdg G = 0 A B 1 A B
5 4 rneqd V W A V B V ran iEdg G = ran 0 A B 1 A B
6 c0ex 0 V
7 1ex 1 V
8 rnpropg 0 V 1 V ran 0 A B 1 A B = A B A B
9 6 7 8 mp2an ran 0 A B 1 A B = A B A B
10 9 a1i V W A V B V ran 0 A B 1 A B = A B A B
11 dfsn2 A B = A B A B
12 10 11 eqtr4di V W A V B V ran 0 A B 1 A B = A B
13 3 5 12 3eqtrd V W A V B V Edg G = A B