Metamath Proof Explorer


Theorem sscrel

Description: The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion sscrel Rel cat

Proof

Step Hyp Ref Expression
1 df-ssc cat = h j | t j Fn t × t s 𝒫 t h x s × s 𝒫 j x
2 1 relopabiv Rel cat