Metamath Proof Explorer

Theorem dfrefrels3

Description: Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019)

		Ref	Expression
	Assertion	dfrefrels3	\|- RefRels = { r e. Rels \| A. x e. dom r A. y e. ran r ( x = y -> x r y ) }

Step	Hyp	Ref	Expression
1		dfrefrels2	\|- RefRels = { r e. Rels \| ( _I i^i ( dom r X. ran r ) ) C_ r }
2		idinxpss	\|- ( ( _I i^i ( dom r X. ran r ) ) C_ r <-> A. x e. dom r A. y e. ran r ( x = y -> x r y ) )
3	1 2	rabbieq	\|- RefRels = { r e. Rels \| A. x e. dom r A. y e. ran r ( x = y -> x r y ) }

Step

Hyp

Ref

Expression

 |-  RefRels = { r e. Rels | ( _I i^i ( dom r X. ran r ) ) C_ r }

 |-  ( ( _I i^i ( dom r X. ran r ) ) C_ r <-> A. x e. dom r A. y e. ran r ( x = y -> x r y ) )

1 2

 |-  RefRels = { r e. Rels | A. x e. dom r A. y e. ran r ( x = y -> x r y ) }