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 C_ B -> ( _I |` A ) C_ ( _I i^i ( A X. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		resss	|- ( _I |` A ) C_ _I
2	1	a1i	|- ( A C_ B -> ( _I |` A ) C_ _I )
3		idssxp	|- ( _I |` A ) C_ ( A X. A )
4		xpss2	|- ( A C_ B -> ( A X. A ) C_ ( A X. B ) )
5	3 4	sstrid	|- ( A C_ B -> ( _I |` A ) C_ ( A X. B ) )
6	2 5	ssind	|- ( A C_ B -> ( _I |` A ) C_ ( _I i^i ( A X. B ) ) )