Description: The cosets by the range Cartesian product with the restricted identity relation are in equivalence relation if and only if the range Cartesian product with the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | detxrnidres | |- ( Disj ( R |X. ( _I |` A ) ) <-> EqvRel ,~ ( R |X. ( _I |` A ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | disjALTVxrnidres | |- Disj ( R |X. ( _I |` A ) ) |
|
2 | 1 | detlem | |- ( Disj ( R |X. ( _I |` A ) ) <-> EqvRel ,~ ( R |X. ( _I |` A ) ) ) |