cossssid2

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	cossssid2	$⊢ ≀ R \subseteq I \leftrightarrow \forall x \forall y (\exists u (u R x \land u R y) \to x = y)$

Step	Hyp	Ref	Expression
1		df-id	$⊢ I = \{⟨x, y⟩ \| x = y\}$
2	1	sseq2i	$⊢ ≀ R \subseteq I \leftrightarrow ≀ R \subseteq \{⟨x, y⟩ \| x = y\}$
3		df-coss	$⊢ ≀ R = \{⟨x, y⟩ \| \exists u (u R x \land u R y)\}$
4	3	sseq1i	$⊢ ≀ R \subseteq \{⟨x, y⟩ \| x = y\} \leftrightarrow \{⟨x, y⟩ \| \exists u (u R x \land u R y)\} \subseteq \{⟨x, y⟩ \| x = y\}$
5		ssopab2bw	$⊢ \{⟨x, y⟩ \| \exists u (u R x \land u R y)\} \subseteq \{⟨x, y⟩ \| x = y\} \leftrightarrow \forall x \forall y (\exists u (u R x \land u R y) \to x = y)$
6	2 4 5	3bitri	$⊢ ≀ R \subseteq I \leftrightarrow \forall x \forall y (\exists u (u R x \land u R y) \to x = y)$

Metamath Proof Explorer