Theorem cossid

Description: Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019)

	Ref	Expression
Assertion	cossid	$$⊢\wr \mathrm{I}=\mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		equvinv	$$⊢y=z\leftrightarrow \exists x\left(x=y\wedge x=z\right)$$
2		ideqg	$$⊢y\in \mathrm{V}\to \left(x\mathrm{I}y\leftrightarrow x=y\right)$$
3	2	elv	$$⊢x\mathrm{I}y\leftrightarrow x=y$$
4		ideqg	$$⊢z\in \mathrm{V}\to \left(x\mathrm{I}z\leftrightarrow x=z\right)$$
5	4	elv	$$⊢x\mathrm{I}z\leftrightarrow x=z$$
6	3 5	anbi12i	$$⊢\left(x\mathrm{I}y\wedge x\mathrm{I}z\right)\leftrightarrow \left(x=y\wedge x=z\right)$$
7	6	exbii	$$⊢\exists x\left(x\mathrm{I}y\wedge x\mathrm{I}z\right)\leftrightarrow \exists x\left(x=y\wedge x=z\right)$$
8	1 7	bitr4i	$$⊢y=z\leftrightarrow \exists x\left(x\mathrm{I}y\wedge x\mathrm{I}z\right)$$
9	8	opabbii	$$⊢\left\{⟨y,z⟩|y=z\right\}=\left\{⟨y,z⟩|\exists x\left(x\mathrm{I}y\wedge x\mathrm{I}z\right)\right\}$$
10		df-id	$$⊢\mathrm{I}=\left\{⟨y,z⟩|y=z\right\}$$
11		df-coss	$$⊢\wr \mathrm{I}=\left\{⟨y,z⟩|\exists x\left(x\mathrm{I}y\wedge x\mathrm{I}z\right)\right\}$$
12	9 10 11	3eqtr4ri	$$⊢\wr \mathrm{I}=\mathrm{I}$$