cossssid4

Description: Equivalent expressions for the class of cosets by R to be a subset of the identity class. (Contributed by Peter Mazsa, 31-Aug-2021)

		Ref	Expression
	Assertion	cossssid4	$⊢ ≀ R \subseteq I \leftrightarrow \forall u \exists^{*} x u R x$

Step	Hyp	Ref	Expression
1		cossssid3	$⊢ ≀ R \subseteq I \leftrightarrow \forall u \forall x \forall y ((u R x \land u R y) \to x = y)$
2		breq2	$⊢ x = y \to (u R x \leftrightarrow u R y)$
3	2	mo4	$⊢ \exists^{*} x u R x \leftrightarrow \forall x \forall y ((u R x \land u R y) \to x = y)$
4	3	albii	$⊢ \forall u \exists^{*} x u R x \leftrightarrow \forall u \forall x \forall y ((u R x \land u R y) \to x = y)$
5	1 4	bitr4i	$⊢ ≀ R \subseteq I \leftrightarrow \forall u \exists^{*} x u R x$

Metamath Proof Explorer