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

Proof

Step Hyp Ref Expression
1 symrelcoss2 
 |-  ( `' ,~ R C_ ,~ R /\ Rel ,~ R )
2 dfsymrel2 
 |-  ( SymRel ,~ R <-> ( `' ,~ R C_ ,~ R /\ Rel ,~ R ) )
3 1 2 mpbir 
 |-  SymRel ,~ R