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 C_ A /\ I = ( B |` dom I ) /\ E C_ ~P 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 e. _V /\ G e. _V ) )
7	1 2 3 4 5	issubgr	|- ( ( G e. _V /\ S e. _V ) -> ( S SubGraph G <-> ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) ) )
8	7	biimpd	|- ( ( G e. _V /\ S e. _V ) -> ( S SubGraph G -> ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) ) )
9	8	ancoms	|- ( ( S e. _V /\ G e. _V ) -> ( S SubGraph G -> ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) ) )
10	6 9	mpcom	|- ( S SubGraph G -> ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) )