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 ) ) |
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 ) ) |