Theorem inxpss2

Description: Two ways to say that intersections with Cartesian products are in a subclass relation. (Contributed by Peter Mazsa, 8-Mar-2019)

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

Proof

Step	Hyp	Ref	Expression
1		relinxp	|- Rel ( R i^i ( A X. B ) )
2		ssrel3	|- ( Rel ( R i^i ( A X. B ) ) -> ( ( R i^i ( A X. B ) ) C_ ( S i^i ( A X. B ) ) <-> A. x A. y ( x ( R i^i ( A X. B ) ) y -> x ( S i^i ( A X. B ) ) y ) ) )
3	1 2	ax-mp	|- ( ( R i^i ( A X. B ) ) C_ ( S i^i ( A X. B ) ) <-> A. x A. y ( x ( R i^i ( A X. B ) ) y -> x ( S i^i ( A X. B ) ) y ) )
4		inxpss3	|- ( A. x A. y ( x ( R i^i ( A X. B ) ) y -> x ( S i^i ( A X. B ) ) y ) <-> A. x e. A A. y e. B ( x R y -> x S y ) )
5	3 4	bitri	|- ( ( R i^i ( A X. B ) ) C_ ( S i^i ( A X. B ) ) <-> A. x e. A A. y e. B ( x R y -> x S y ) )