Metamath Proof Explorer

Theorem coi2ss

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

Ref Expression
Assertion coi2ss 
|- ( _I o. A ) C_ A

Proof

Step Hyp Ref Expression
1 coi2res 
 |-  ( _I o. A ) = ( A |` _V )
2 resss 
 |-  ( A |` _V ) C_ A
3 1 2 eqsstri 
 |-  ( _I o. A ) C_ A