This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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