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 \leftrightarrow (\forall x \in (dom R \cap ran R) x R x \land Rel R)$

Step	Hyp	Ref	Expression
1		dfrefrel2	$⊢ RefRel R \leftrightarrow (I \cap (dom R \times ran R) \subseteq R \land Rel R)$
2		ref5	$⊢ I \cap (dom R \times ran R) \subseteq R \leftrightarrow \forall x \in (dom R \cap ran R) x R x$
3	1 2	bianbi	$⊢ RefRel R \leftrightarrow (\forall x \in (dom R \cap ran R) x R x \land Rel R)$