Theorem coi1ss

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

	Ref	Expression
Assertion	coi1ss	$$⊢A\circ \mathrm{I}\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		coi1res	$$⊢A\circ \mathrm{I}={A\upharpoonright }_{\mathrm{V}}$$
2		resss	$$⊢{A\upharpoonright }_{\mathrm{V}}\subseteq A$$
3	1 2	eqsstri	$$⊢A\circ \mathrm{I}\subseteq A$$