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