Metamath Proof Explorer


Theorem symrelcoss3

Description: The class of cosets by R is symmetric, see dfsymrel3 . (Contributed by Peter Mazsa, 28-Mar-2019) (Revised by Peter Mazsa, 17-Sep-2021)

Ref Expression
Assertion symrelcoss3 x y x R y y R x Rel R

Proof

Step Hyp Ref Expression
1 brcosscnvcoss x V y V x R y y R x
2 1 el2v x R y y R x
3 2 biimpi x R y y R x
4 3 gen2 x y x R y y R x
5 relcoss Rel R
6 4 5 pm3.2i x y x R y y R x Rel R