cossssid3

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

		Ref	Expression
	Assertion	cossssid3	$⊢ ≀ R \subseteq I \leftrightarrow \forall u \forall x \forall y ((u R x \land u R y) \to x = y)$

Step	Hyp	Ref	Expression
1		cossssid2	$⊢ ≀ R \subseteq I \leftrightarrow \forall x \forall y (\exists u (u R x \land u R y) \to x = y)$
2		19.23v	$⊢ \forall u ((u R x \land u R y) \to x = y) \leftrightarrow (\exists u (u R x \land u R y) \to x = y)$
3	2	albii	$⊢ \forall y \forall u ((u R x \land u R y) \to x = y) \leftrightarrow \forall y (\exists u (u R x \land u R y) \to x = y)$
4		alcom	$⊢ \forall y \forall u ((u R x \land u R y) \to x = y) \leftrightarrow \forall u \forall y ((u R x \land u R y) \to x = y)$
5	3 4	bitr3i	$⊢ \forall y (\exists u (u R x \land u R y) \to x = y) \leftrightarrow \forall u \forall y ((u R x \land u R y) \to x = y)$
6	5	albii	$⊢ \forall x \forall y (\exists u (u R x \land u R y) \to x = y) \leftrightarrow \forall x \forall u \forall y ((u R x \land u R y) \to x = y)$
7		alcom	$⊢ \forall x \forall u \forall y ((u R x \land u R y) \to x = y) \leftrightarrow \forall u \forall x \forall y ((u R x \land u R y) \to x = y)$
8	1 6 7	3bitri	$⊢ ≀ R \subseteq I \leftrightarrow \forall u \forall x \forall y ((u R x \land u R y) \to x = y)$

Metamath Proof Explorer