# 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 Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cR
|-  R
1 cA
|-  A
2 1 0 wer
|-  R Er A
3 0 wrel
|-  Rel R
4 0 cdm
|-  dom R
5 4 1 wceq
|-  dom R = A
6 0 ccnv
|-  `' R
7 0 0 ccom
|-  ( R o. R )
8 6 7 cun
|-  ( `' R u. ( R o. R ) )
9 8 0 wss
|-  ( `' R u. ( R o. R ) ) C_ R
10 3 5 9 w3a
|-  ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R )
11 2 10 wb
|-  ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )