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 }