Theorem coi1ss

Description: Precomposing with the identity yields a subclass. (Contributed by BJ, 8-Nov-2026) Can shorten mvdco .

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

Proof

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