Metamath Proof Explorer

Theorem elsymrels5

Description: Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021)

Ref Expression
Assertion elsymrels5 
|- ( R e. SymRels <-> ( A. x A. y ( x R y <-> y R x ) /\ R e. Rels ) )

Proof

Step Hyp Ref Expression
1 dfsymrels5 
 |-  SymRels = { r e. Rels | A. x A. y ( x r y <-> y r x ) }
2 breq 
 |-  ( r = R -> ( x r y <-> x R y ) )
3 breq 
 |-  ( r = R -> ( y r x <-> y R x ) )
4 2 3 bibi12d 
 |-  ( r = R -> ( ( x r y <-> y r x ) <-> ( x R y <-> y R x ) ) )
5 4 2albidv 
 |-  ( r = R -> ( A. x A. y ( x r y <-> y r x ) <-> A. x A. y ( x R y <-> y R x ) ) )
6 1 5 rabeqel 
 |-  ( R e. SymRels <-> ( A. x A. y ( x R y <-> y R x ) /\ R e. Rels ) )