MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-er Structured version   Visualization version   GIF version

Definition df-er 7629
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 7630 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 7649, ersymb 7643, and ertr 7644. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 2-Nov-2015.)
Assertion
Ref Expression
df-er (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))

Detailed syntax breakdown of Definition df-er
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wer 7626 . 2 wff 𝑅 Er 𝐴
42wrel 5043 . . 3 wff Rel 𝑅
52cdm 5038 . . . 4 class dom 𝑅
65, 1wceq 1475 . . 3 wff dom 𝑅 = 𝐴
72ccnv 5037 . . . . 5 class 𝑅
82, 2ccom 5042 . . . . 5 class (𝑅𝑅)
97, 8cun 3538 . . . 4 class (𝑅 ∪ (𝑅𝑅))
109, 2wss 3540 . . 3 wff (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅
114, 6, 10w3a 1031 . 2 wff (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
123, 11wb 195 1 wff (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
Colors of variables: wff setvar class
This definition is referenced by:  dfer2  7630  ereq1  7636  ereq2  7637  errel  7638  erdm  7639  ersym  7641  ertr  7644  xpider  7705  fcoinver  28798
  Copyright terms: Public domain W3C validator