Description: Two ways to say that an intersection of the identity relation with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | idinxpss | |- ( ( _I i^i ( A X. B ) ) C_ R <-> A. x e. A A. y e. B ( x = y -> x R y ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inxpss | |- ( ( _I i^i ( A X. B ) ) C_ R <-> 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 <-> A. x e. A A. y e. B ( x = y -> x R y ) ) |