Theorem sscid

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

	Ref	Expression
Assertion	sscid	|- ( ( H Fn ( S X. S ) /\ S e. V ) -> H C_cat H )

Proof

Step	Hyp	Ref	Expression
1		fnresdm	|- ( H Fn ( S X. S ) -> ( H |` ( S X. S ) ) = H )
2	1	adantr	|- ( ( H Fn ( S X. S ) /\ S e. V ) -> ( H |` ( S X. S ) ) = H )
3		sscres	|- ( ( H Fn ( S X. S ) /\ S e. V ) -> ( H |` ( S X. S ) ) C_cat H )
4	2 3	eqbrtrrd	|- ( ( H Fn ( S X. S ) /\ S e. V ) -> H C_cat H )