This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem refrelcoss

Description: The class of cosets by R is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020)

		Ref	Expression
	Assertion	refrelcoss	$⊢ RefRel ≀ R$

Step	Hyp	Ref	Expression
1		refrelcoss2	$⊢ (I \cap (dom ≀ R \times ran ≀ R) \subseteq ≀ R \land Rel ≀ R)$
2		dfrefrel2	$⊢ RefRel ≀ R \leftrightarrow (I \cap (dom ≀ R \times ran ≀ R) \subseteq ≀ R \land Rel ≀ R)$
3	1 2	mpbir	$⊢ RefRel ≀ R$