Description: The properties of a subgraph: If S is a subgraph of G , its vertices are also vertices of G , and its edges are also edges of G . (Contributed by AV, 19-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | subgrprop3.v | |
|
subgrprop3.a | |
||
subgrprop3.e | |
||
subgrprop3.b | |
||
Assertion | subgrprop3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subgrprop3.v | |
|
2 | subgrprop3.a | |
|
3 | subgrprop3.e | |
|
4 | subgrprop3.b | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | 1 2 5 6 3 | subgrprop2 | |
8 | 3simpa | |
|
9 | 7 8 | syl | |
10 | simprl | |
|
11 | rnss | |
|
12 | 11 | ad2antll | |
13 | subgrv | |
|
14 | edgval | |
|
15 | 14 | a1i | |
16 | 3 15 | eqtrid | |
17 | edgval | |
|
18 | 17 | a1i | |
19 | 4 18 | eqtrid | |
20 | 16 19 | sseq12d | |
21 | 13 20 | syl | |
22 | 21 | adantr | |
23 | 12 22 | mpbird | |
24 | 10 23 | jca | |
25 | 9 24 | mpdan | |