This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relsubgr

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

		Ref	Expression
	Assertion	relsubgr	$⊢ Rel SubGraph$

Step	Hyp	Ref	Expression
1		df-subgr	$⊢ SubGraph = \{⟨s, g⟩ \| (Vtx (s) \subseteq Vtx (g) \land iEdg (s) = {iEdg (g) ↾}_{dom iEdg (s)} \land Edg (s) \subseteq 𝒫 Vtx (s))\}$
2	1	relopabiv	$⊢ Rel SubGraph$