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 e. Rels | A. x A. y ( x r y <-> y r x ) }

Proof

Step Hyp Ref Expression
1 dfsymrels4 
 |-  SymRels = { r e. Rels | `' r = r }
2 elrelscnveq2 
 |-  ( r e. Rels -> ( `' r = r <-> A. x A. y ( x r y <-> y r x ) ) )
3 1 2 rabimbieq 
 |-  SymRels = { r e. Rels | A. x A. y ( x r y <-> y r x ) }