Metamath Proof Explorer


Theorem elsymrels2

Description: Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021)

Ref Expression
Assertion elsymrels2 RSymRelsR-1RRRels

Proof

Step Hyp Ref Expression
1 dfsymrels2 SymRels=rRels|r-1r
2 cnveq r=Rr-1=R-1
3 id r=Rr=R
4 2 3 sseq12d r=Rr-1rR-1R
5 1 4 rabeqel RSymRelsR-1RRRels