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 = { ⟨ 𝑠 , 𝑔 ⟩ ∣ ( ( Vtx ‘ 𝑠 ) ⊆ ( Vtx ‘ 𝑔 ) ∧ ( iEdg ‘ 𝑠 ) = ( ( iEdg ‘ 𝑔 ) ↾ dom ( iEdg ‘ 𝑠 ) ) ∧ ( Edg ‘ 𝑠 ) ⊆ 𝒫 ( Vtx ‘ 𝑠 ) ) }
2	1	relopabiv	⊢ Rel SubGraph