symrelcoss2

Description: The class of cosets by R is symmetric, see dfsymrel2 . (Contributed by Peter Mazsa, 27-Dec-2018)

		Ref	Expression
	Assertion	symrelcoss2	$⊢ ({≀ R}^{-1} \subseteq ≀ R \land Rel ≀ R)$

Step	Hyp	Ref	Expression
1		symrelcoss3	$⊢ (\forall x \forall y (x ≀ R y \to y ≀ R x) \land Rel ≀ R)$
2		cnvsym	$⊢ {≀ R}^{-1} \subseteq ≀ R \leftrightarrow \forall x \forall y (x ≀ R y \to y ≀ R x)$
3	2	anbi1i	$⊢ ({≀ R}^{-1} \subseteq ≀ R \land Rel ≀ R) \leftrightarrow (\forall x \forall y (x ≀ R y \to y ≀ R x) \land Rel ≀ R)$
4	1 3	mpbir	$⊢ ({≀ R}^{-1} \subseteq ≀ R \land Rel ≀ R)$

Metamath Proof Explorer