Theorem cossid

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

	Ref	Expression
Assertion	cossid	⊢ ≀ I = I

Proof

Step	Hyp	Ref	Expression
1		equvinv	⊢ ( 𝑦 = 𝑧 ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑧 ) )
2		ideqg	⊢ ( 𝑦 ∈ V → ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 ) )
3	2	elv	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
4		ideqg	⊢ ( 𝑧 ∈ V → ( 𝑥 I 𝑧 ↔ 𝑥 = 𝑧 ) )
5	4	elv	⊢ ( 𝑥 I 𝑧 ↔ 𝑥 = 𝑧 )
6	3 5	anbi12i	⊢ ( ( 𝑥 I 𝑦 ∧ 𝑥 I 𝑧 ) ↔ ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑧 ) )
7	6	exbii	⊢ ( ∃ 𝑥 ( 𝑥 I 𝑦 ∧ 𝑥 I 𝑧 ) ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑧 ) )
8	1 7	bitr4i	⊢ ( 𝑦 = 𝑧 ↔ ∃ 𝑥 ( 𝑥 I 𝑦 ∧ 𝑥 I 𝑧 ) )
9	8	opabbii	⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑦 = 𝑧 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑥 I 𝑦 ∧ 𝑥 I 𝑧 ) }
10		df-id	⊢ I = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑦 = 𝑧 }
11		df-coss	⊢ ≀ I = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑥 I 𝑦 ∧ 𝑥 I 𝑧 ) }
12	9 10 11	3eqtr4ri	⊢ ≀ I = I