Metamath Proof Explorer


Theorem idinxpssinxp

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

Ref Expression
Assertion idinxpssinxp I A × B R A × B x A y B x = y x R y

Proof

Step Hyp Ref Expression
1 inxpss2 I A × B R A × B x A y B x I y x R y
2 ideqg y V x I y x = y
3 2 elv x I y x = y
4 3 imbi1i x I y x R y x = y x R y
5 4 2ralbii x A y B x I y x R y x A y B x = y x R y
6 1 5 bitri I A × B R A × B x A y B x = y x R y