Theorem inxpssidinxp

Description: Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 . (Contributed by Peter Mazsa, 4-Jul-2019)

	Ref	Expression
Assertion	inxpssidinxp	|- ( ( R i^i ( A X. B ) ) C_ ( _I i^i ( A X. B ) ) <-> A. x e. A A. y e. B ( x R y -> x = y ) )

Proof

Step	Hyp	Ref	Expression
1		inxpss2	|- ( ( R i^i ( A X. B ) ) C_ ( _I i^i ( A X. B ) ) <-> A. x e. A A. y e. B ( x R y -> x _I y ) )
2		ideqg	|- ( y e. _V -> ( x _I y <-> x = y ) )
3	2	elv	|- ( x _I y <-> x = y )
4	3	imbi2i	|- ( ( x R y -> x _I y ) <-> ( x R y -> x = y ) )
5	4	2ralbii	|- ( A. x e. A A. y e. B ( x R y -> x _I y ) <-> A. x e. A A. y e. B ( x R y -> x = y ) )
6	1 5	bitri	|- ( ( R i^i ( A X. B ) ) C_ ( _I i^i ( A X. B ) ) <-> A. x e. A A. y e. B ( x R y -> x = y ) )