Metamath Proof Explorer


Theorem idreseqidinxp

Description: Condition for the identity restriction to be equal to the identity intersection with a Cartesian product. (Contributed by Peter Mazsa, 19-Jul-2018)

Ref Expression
Assertion idreseqidinxp
|- ( A C_ B -> ( _I i^i ( A X. B ) ) = ( _I |` A ) )

Proof

Step Hyp Ref Expression
1 inxpssres
 |-  ( _I i^i ( A X. B ) ) C_ ( _I |` A )
2 1 a1i
 |-  ( A C_ B -> ( _I i^i ( A X. B ) ) C_ ( _I |` A ) )
3 idresssidinxp
 |-  ( A C_ B -> ( _I |` A ) C_ ( _I i^i ( A X. B ) ) )
4 2 3 eqssd
 |-  ( A C_ B -> ( _I i^i ( A X. B ) ) = ( _I |` A ) )