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 C_cat

Proof

Step Hyp Ref Expression
1 df-ssc 
 |-  C_cat = { <. h , j >. | E. t ( j Fn ( t X. t ) /\ E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) ) }
2 1 relopabiv 
 |-  Rel C_cat