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 SymRels x y x R y y R x R Rels

Proof

Step Hyp Ref Expression
1 dfsymrels5 SymRels = r Rels | x 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 x y x r y y r x x y x R y y R x
6 1 5 rabeqel R SymRels x y x R y y R x R Rels