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 i^i ( A X. B ) ) C_ ( R i^i ( A X. B ) ) <-> A. x e. A A. y e. B ( x = y -> x R y ) )

Proof

Step Hyp Ref Expression
1 inxpss2
 |-  ( ( _I i^i ( A X. B ) ) C_ ( R i^i ( A X. B ) ) <-> A. x e. A A. y e. B ( x _I y -> x R y ) )
2 ideqg
 |-  ( y e. _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
 |-  ( A. x e. A A. y e. B ( x _I y -> x R y ) <-> A. x e. A A. y e. B ( x = y -> x R y ) )
6 1 5 bitri
 |-  ( ( _I i^i ( A X. B ) ) C_ ( R i^i ( A X. B ) ) <-> A. x e. A A. y e. B ( x = y -> x R y ) )