Theorem relsubgr

Description: The class of the subgraph relation is a relation. (Contributed by AV, 16-Nov-2020)

	Ref	Expression
Assertion	relsubgr	|- Rel SubGraph

Proof

Step	Hyp	Ref	Expression
1		df-subgr	|- SubGraph = { <. s , g >. | ( ( Vtx ` s ) C_ ( Vtx ` g ) /\ ( iEdg ` s ) = ( ( iEdg ` g ) |` dom ( iEdg ` s ) ) /\ ( Edg ` s ) C_ ~P ( Vtx ` s ) ) }
2	1	relopabiv	|- Rel SubGraph