Metamath Proof Explorer


Theorem elrelscnveq4

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021)

Ref Expression
Assertion elrelscnveq4 R Rels R -1 R x y x R y y R x

Proof

Step Hyp Ref Expression
1 elrelscnveq R Rels R -1 R R -1 = R
2 elrelscnveq2 R Rels R -1 = R x y x R y y R x
3 1 2 bitrd R Rels R -1 R x y x R y y R x