Theorem 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	$$⊢\wr R\subseteq \mathrm{I}\leftrightarrow \forall x\forall y\left(\exists u\left(uRx\wedge uRy\right)\to x=y\right)$$

Proof

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