Theorem relsubgr

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

	Ref	Expression
Assertion	relsubgr	$$⊢\mathrm{Rel}\mathrm{SubGraph}$$

Proof

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