Metamath Proof Explorer


Theorem dfsymrels4

Description: Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019)

Ref Expression
Assertion dfsymrels4 SymRels = r Rels | r -1 = r

Proof

Step Hyp Ref Expression
1 dfsymrels2 SymRels = r Rels | r -1 r
2 elrelscnveq r Rels r -1 r r -1 = r
3 1 2 rabimbieq SymRels = r Rels | r -1 = r