Database
GRAPH THEORY
Undirected graphs
Subgraphs
subgrprop
Next ⟩
subgrprop2
Metamath Proof Explorer
Ascii
Unicode
Theorem
subgrprop
Description:
The properties of a subgraph.
(Contributed by
AV
, 19-Nov-2020)
Ref
Expression
Hypotheses
issubgr.v
⊢
V
=
Vtx
⁡
S
issubgr.a
⊢
A
=
Vtx
⁡
G
issubgr.i
⊢
I
=
iEdg
⁡
S
issubgr.b
⊢
B
=
iEdg
⁡
G
issubgr.e
⊢
E
=
Edg
⁡
S
Assertion
subgrprop
⊢
S
SubGraph
G
→
V
⊆
A
∧
I
=
B
↾
dom
⁡
I
∧
E
⊆
𝒫
V
Proof
Step
Hyp
Ref
Expression
1
issubgr.v
⊢
V
=
Vtx
⁡
S
2
issubgr.a
⊢
A
=
Vtx
⁡
G
3
issubgr.i
⊢
I
=
iEdg
⁡
S
4
issubgr.b
⊢
B
=
iEdg
⁡
G
5
issubgr.e
⊢
E
=
Edg
⁡
S
6
subgrv
⊢
S
SubGraph
G
→
S
∈
V
∧
G
∈
V
7
1
2
3
4
5
issubgr
⊢
G
∈
V
∧
S
∈
V
→
S
SubGraph
G
↔
V
⊆
A
∧
I
=
B
↾
dom
⁡
I
∧
E
⊆
𝒫
V
8
7
biimpd
⊢
G
∈
V
∧
S
∈
V
→
S
SubGraph
G
→
V
⊆
A
∧
I
=
B
↾
dom
⁡
I
∧
E
⊆
𝒫
V
9
8
ancoms
⊢
S
∈
V
∧
G
∈
V
→
S
SubGraph
G
→
V
⊆
A
∧
I
=
B
↾
dom
⁡
I
∧
E
⊆
𝒫
V
10
6
9
mpcom
⊢
S
SubGraph
G
→
V
⊆
A
∧
I
=
B
↾
dom
⁡
I
∧
E
⊆
𝒫
V