Metamath Proof Explorer


Theorem 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 R Rel R

Proof

Step Hyp Ref Expression
1 symrelcoss3 x y x R y y R x Rel R
2 cnvsym R -1 R x y x R y y R x
3 2 anbi1i R -1 R Rel R x y x R y y R x Rel R
4 1 3 mpbir R -1 R Rel R