Theorem coi2ss

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

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

Proof

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