Metamath Proof Explorer


Theorem elsymrels2

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

Ref Expression
Assertion elsymrels2 R SymRels R -1 R R Rels

Proof

Step Hyp Ref Expression
1 dfsymrels2 SymRels = r Rels | r -1 r
2 cnveq r = R r -1 = R -1
3 id r = R r = R
4 2 3 sseq12d r = R r -1 r R -1 R
5 1 4 rabeqel R SymRels R -1 R R Rels