Metamath Proof Explorer


Theorem dfsymrels5

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

Ref Expression
Assertion dfsymrels5 SymRels = r Rels | x y x r y y r x

Proof

Step Hyp Ref Expression
1 dfsymrels4 SymRels = r Rels | r -1 = r
2 elrelscnveq2 r Rels r -1 = r x y x r y y r x
3 1 2 rabimbieq SymRels = r Rels | x y x r y y r x