Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Equivalence relations
eqvrelsymrel
Next ⟩
eqvreltrrel
Metamath Proof Explorer
Ascii
Unicode
Theorem
eqvrelsymrel
Description:
An equivalence relation is symmetric.
(Contributed by
Peter Mazsa
, 29-Dec-2021)
Ref
Expression
Assertion
eqvrelsymrel
⊢
EqvRel
R
→
SymRel
R
Proof
Step
Hyp
Ref
Expression
1
df-eqvrel
⊢
EqvRel
R
↔
RefRel
R
∧
SymRel
R
∧
TrRel
R
2
1
simp2bi
⊢
EqvRel
R
→
SymRel
R