Metamath Proof Explorer


Theorem subgrprop3

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 V=VtxS
subgrprop3.a A=VtxG
subgrprop3.e E=EdgS
subgrprop3.b B=EdgG
Assertion subgrprop3 SSubGraphGVAEB

Proof

Step Hyp Ref Expression
1 subgrprop3.v V=VtxS
2 subgrprop3.a A=VtxG
3 subgrprop3.e E=EdgS
4 subgrprop3.b B=EdgG
5 eqid iEdgS=iEdgS
6 eqid iEdgG=iEdgG
7 1 2 5 6 3 subgrprop2 SSubGraphGVAiEdgSiEdgGE𝒫V
8 3simpa VAiEdgSiEdgGE𝒫VVAiEdgSiEdgG
9 7 8 syl SSubGraphGVAiEdgSiEdgG
10 simprl SSubGraphGVAiEdgSiEdgGVA
11 rnss iEdgSiEdgGraniEdgSraniEdgG
12 11 ad2antll SSubGraphGVAiEdgSiEdgGraniEdgSraniEdgG
13 subgrv SSubGraphGSVGV
14 edgval EdgS=raniEdgS
15 14 a1i SVGVEdgS=raniEdgS
16 3 15 eqtrid SVGVE=raniEdgS
17 edgval EdgG=raniEdgG
18 17 a1i SVGVEdgG=raniEdgG
19 4 18 eqtrid SVGVB=raniEdgG
20 16 19 sseq12d SVGVEBraniEdgSraniEdgG
21 13 20 syl SSubGraphGEBraniEdgSraniEdgG
22 21 adantr SSubGraphGVAiEdgSiEdgGEBraniEdgSraniEdgG
23 12 22 mpbird SSubGraphGVAiEdgSiEdgGEB
24 10 23 jca SSubGraphGVAiEdgSiEdgGVAEB
25 9 24 mpdan SSubGraphGVAEB