Theorem coi2ss

Description: Postcomposing with the identity yields a subclass. (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	coi2ss	⊢ ( I ∘ 𝐴 ) ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		coi2res	⊢ ( I ∘ 𝐴 ) = ( 𝐴 ↾ V )
2		resss	⊢ ( 𝐴 ↾ V ) ⊆ 𝐴
3	1 2	eqsstri	⊢ ( I ∘ 𝐴 ) ⊆ 𝐴