Metamath Proof Explorer

Theorem coi1ss

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

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

Proof

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