Metamath Proof Explorer


Theorem dfsymrel5

Description: Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021)

Ref Expression
Assertion dfsymrel5 SymRel R x y x R y y R x Rel R

Proof

Step Hyp Ref Expression
1 dfsymrel2 SymRel R R -1 R Rel R
2 relcnveq4 Rel R R -1 R x y x R y y R x
3 2 pm5.32ri R -1 R Rel R x y x R y y R x Rel R
4 1 3 bitri SymRel R x y x R y y R x Rel R