Metamath Proof Explorer

Theorem dfrefrel5

Description: Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 12-Dec-2023)

		Ref	Expression
	Assertion	dfrefrel5	\|- ( RefRel R <-> ( A. x e. ( dom R i^i ran R ) x R x /\ Rel R ) )

Step	Hyp	Ref	Expression
1		dfrefrel2	\|- ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) )
2		ref5	\|- ( ( _I i^i ( dom R X. ran R ) ) C_ R <-> A. x e. ( dom R i^i ran R ) x R x )
3	1 2	bianbi	\|- ( RefRel R <-> ( A. x e. ( dom R i^i ran R ) x R x /\ Rel R ) )

Step

Hyp

Ref

Expression

 |-  ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) )

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

1 2

 |-  ( RefRel R <-> ( A. x e. ( dom R i^i ran R ) x R x /\ Rel R ) )