Metamath Proof Explorer


Theorem inxpss3

Description: Two ways to say that an intersection with a Cartesian product is a subclass (see also inxpss ). (Contributed by Peter Mazsa, 8-Mar-2019)

Ref Expression
Assertion inxpss3 x y x R A × B y x S A × B y 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 brinxp2 x S A × B y x A y B x S y
3 1 2 imbi12i x R A × B y x S A × B y x A y B x R y x A y B x S y
4 imdistan x A y B x R y x S y x A y B x R y x A y B x S y
5 3 4 bitr4i x R A × B y x S A × B y x A y B x R y x S y
6 5 2albii x y x R A × B y x S A × B y x y x A y B x R y x S y
7 r2al x A y B x R y x S y x y x A y B x R y x S y
8 6 7 bitr4i x y x R A × B y x S A × B y x A y B x R y x S y