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 e. Rels | `' r = r }

Proof

Step Hyp Ref Expression
1 dfsymrels2
 |-  SymRels = { r e. Rels | `' r C_ r }
2 elrelscnveq
 |-  ( r e. Rels -> ( `' r C_ r <-> `' r = r ) )
3 1 2 rabimbieq
 |-  SymRels = { r e. Rels | `' r = r }