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	|- ( y = z <-> E. x ( x = y /\ x = z ) )
2		ideqg	|- ( y e. _V -> ( x _I y <-> x = y ) )
3	2	elv	|- ( x _I y <-> x = y )
4		ideqg	|- ( z e. _V -> ( x _I z <-> x = z ) )
5	4	elv	|- ( x _I z <-> x = z )
6	3 5	anbi12i	|- ( ( x _I y /\ x _I z ) <-> ( x = y /\ x = z ) )
7	6	exbii	|- ( E. x ( x _I y /\ x _I z ) <-> E. x ( x = y /\ x = z ) )
8	1 7	bitr4i	|- ( y = z <-> E. x ( x _I y /\ x _I z ) )
9	8	opabbii	|- { <. y , z >. | y = z } = { <. y , z >. | E. x ( x _I y /\ x _I z ) }
10		df-id	|- _I = { <. y , z >. | y = z }
11		df-coss	|- ,~ _I = { <. y , z >. | E. x ( x _I y /\ x _I z ) }
12	9 10 11	3eqtr4ri	|- ,~ _I = _I