Metamath Proof Explorer


Theorem idresssidinxp

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

Ref Expression
Assertion idresssidinxp A B I A I A × B

Proof

Step Hyp Ref Expression
1 resss I A I
2 1 a1i A B I A I
3 idssxp I A A × A
4 xpss2 A B A × A A × B
5 3 4 sstrid A B I A A × B
6 2 5 ssind A B I A I A × B