Description: The property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isumgr.v | |
|
isumgr.e | |
||
Assertion | isumgr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isumgr.v | |
|
2 | isumgr.e | |
|
3 | df-umgr | |
|
4 | 3 | eleq2i | |
5 | fveq2 | |
|
6 | 5 2 | eqtr4di | |
7 | 5 | dmeqd | |
8 | 2 | eqcomi | |
9 | 8 | dmeqi | |
10 | 7 9 | eqtrdi | |
11 | fveq2 | |
|
12 | 11 1 | eqtr4di | |
13 | 12 | pweqd | |
14 | 13 | difeq1d | |
15 | 14 | rabeqdv | |
16 | 6 10 15 | feq123d | |
17 | fvexd | |
|
18 | fveq2 | |
|
19 | fvexd | |
|
20 | fveq2 | |
|
21 | 20 | adantr | |
22 | simpr | |
|
23 | 22 | dmeqd | |
24 | pweq | |
|
25 | 24 | ad2antlr | |
26 | 25 | difeq1d | |
27 | 26 | rabeqdv | |
28 | 22 23 27 | feq123d | |
29 | 19 21 28 | sbcied2 | |
30 | 17 18 29 | sbcied2 | |
31 | 30 | cbvabv | |
32 | 16 31 | elab2g | |
33 | 4 32 | syl5bb | |