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
|- ( A. x A. y ( x ,~ R y -> y ,~ R x ) /\ Rel ,~ R )

Proof

Step Hyp Ref Expression
1 brcosscnvcoss
 |-  ( ( x e. _V /\ y e. _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
 |-  A. x A. y ( x ,~ R y -> y ,~ R x )
5 relcoss
 |-  Rel ,~ R
6 4 5 pm3.2i
 |-  ( A. x A. y ( x ,~ R y -> y ,~ R x ) /\ Rel ,~ R )