Theorem detxrnidres

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

Proof

Step	Hyp	Ref	Expression
1		disjALTVxrnidres	|- Disj ( R |X. ( _I |` A ) )
2	1	detlem	|- ( Disj ( R |X. ( _I |` A ) ) <-> EqvRel ,~ ( R |X. ( _I |` A ) ) )