cossid

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

		Ref	Expression
	Assertion	cossid	$⊢ ≀ I = I$

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

Metamath Proof Explorer