# Metamath Proof Explorer

## Definition df-er

Description: Define the equivalence relation predicate. Our notation is not standard. A formal notation doesn't seem to exist in the literature; instead only informal English tends to be used. The present definition, although somewhat cryptic, nicely avoids dummy variables. In dfer2 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref , ersymb , and ertr . (Contributed by NM, 4-Jun-1995) (Revised by Mario Carneiro, 2-Nov-2015)

Ref Expression
Assertion df-er ${⊢}{R}\mathrm{Er}{A}↔\left(\mathrm{Rel}{R}\wedge \mathrm{dom}{R}={A}\wedge {{R}}^{-1}\cup \left({R}\circ {R}\right)\subseteq {R}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cR ${class}{R}$
1 cA ${class}{A}$
2 1 0 wer ${wff}{R}\mathrm{Er}{A}$
3 0 wrel ${wff}\mathrm{Rel}{R}$
4 0 cdm ${class}\mathrm{dom}{R}$
5 4 1 wceq ${wff}\mathrm{dom}{R}={A}$
6 0 ccnv ${class}{{R}}^{-1}$
7 0 0 ccom ${class}\left({R}\circ {R}\right)$
8 6 7 cun ${class}\left({{R}}^{-1}\cup \left({R}\circ {R}\right)\right)$
9 8 0 wss ${wff}{{R}}^{-1}\cup \left({R}\circ {R}\right)\subseteq {R}$
10 3 5 9 w3a ${wff}\left(\mathrm{Rel}{R}\wedge \mathrm{dom}{R}={A}\wedge {{R}}^{-1}\cup \left({R}\circ {R}\right)\subseteq {R}\right)$
11 2 10 wb ${wff}\left({R}\mathrm{Er}{A}↔\left(\mathrm{Rel}{R}\wedge \mathrm{dom}{R}={A}\wedge {{R}}^{-1}\cup \left({R}\circ {R}\right)\subseteq {R}\right)\right)$