Metamath Proof Explorer


Theorem inxpss

Description: Two ways to say that an intersection with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019)

Ref Expression
Assertion inxpss R A × B S x A y B x R y x S y

Proof

Step Hyp Ref Expression
1 brinxp2 x R A × B y x A y B x R y
2 1 imbi1i x R A × B y x S y x A y B x R y x S y
3 impexp x A y B x R y x S y x A y B x R y x S y
4 2 3 bitri x R A × B y x S y x A y B x R y x S y
5 4 2albii x y x R A × B y x S y x y x A y B x R y x S y
6 relinxp Rel R A × B
7 ssrel3 Rel R A × B R A × B S x y x R A × B y x S y
8 6 7 ax-mp R A × B S x y x R A × B y x S y
9 r2al x A y B x R y x S y x y x A y B x R y x S y
10 5 8 9 3bitr4i R A × B S x A y B x R y x S y