Metamath Proof Explorer

Theorem cossssid5

Description: Equivalent expressions for the class of cosets by R to be a subset of the identity class. (Contributed by Peter Mazsa, 5-Sep-2021)

		Ref	Expression
	Assertion	cossssid5	\|- ( ,~ R C_ _I <-> A. x e. ran R A. y e. ran R ( x = y \/ ( [ x ] `' R i^i [ y ] `' R ) = (/) ) )

Step	Hyp	Ref	Expression
1		cossssid4	\|- ( ,~ R C_ _I <-> A. u E* x u R x )
2		ineccnvmo2	\|- ( A. x e. ran R A. y e. ran R ( x = y \/ ( [ x ] `' R i^i [ y ] `' R ) = (/) ) <-> A. u E* x u R x )
3	1 2	bitr4i	\|- ( ,~ R C_ _I <-> A. x e. ran R A. y e. ran R ( x = y \/ ( [ x ] `' R i^i [ y ] `' R ) = (/) ) )

Step

Hyp

Ref

Expression

 |-  ( ,~ R C_ _I <-> A. u E* x u R x )

 |-  ( A. x e. ran R A. y e. ran R ( x = y \/ ( [ x ] `' R i^i [ y ] `' R ) = (/) ) <-> A. u E* x u R x )

1 2

 |-  ( ,~ R C_ _I <-> A. x e. ran R A. y e. ran R ( x = y \/ ( [ x ] `' R i^i [ y ] `' R ) = (/) ) )