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

Metamath Proof Explorer

Theorem symrelcoss

Description: The class of cosets by R is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021)

		Ref	Expression
	Assertion	symrelcoss	$⊢ SymRel ≀ R$

Step	Hyp	Ref	Expression
1		symrelcoss2	$⊢ ({≀ R}^{-1} \subseteq ≀ R \land Rel ≀ R)$
2		dfsymrel2	$⊢ SymRel ≀ R \leftrightarrow ({≀ R}^{-1} \subseteq ≀ R \land Rel ≀ R)$
3	1 2	mpbir	$⊢ SymRel ≀ R$