Metamath Proof Explorer


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 A × B S A × B x A y B x R y x S y

Proof

Step Hyp Ref Expression
1 relinxp Rel R A × B
2 ssrel3 Rel R A × B R A × B S A × B x y x R A × B y x S A × B y
3 1 2 ax-mp R A × B S A × B x y x R A × B y x S A × B y
4 inxpss3 x y x R A × B y x S A × B y x A y B x R y x S y
5 3 4 bitri R A × B S A × B x A y B x R y x S y