Metamath Proof Explorer


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