Metamath Proof Explorer


Theorem eqvrelsymrel

Description: An equivalence relation is symmetric. (Contributed by Peter Mazsa, 29-Dec-2021)

Ref Expression
Assertion eqvrelsymrel EqvRelRSymRelR

Proof

Step Hyp Ref Expression
1 df-eqvrel EqvRelRRefRelRSymRelRTrRelR
2 1 simp2bi EqvRelRSymRelR