|   | Mathbox for Peter Mazsa | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-eqvrels | Structured version Visualization version GIF version | ||
| Description: Define the class of equivalence relations. For sets, being an element of the class of equivalence relations is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel 38595. Alternate definitions are dfeqvrels2 38589 and dfeqvrels3 38590. (Contributed by Peter Mazsa, 7-Nov-2018.) | 
| Ref | Expression | 
|---|---|
| df-eqvrels | ⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels ) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ceqvrels 38198 | . 2 class EqvRels | |
| 2 | crefrels 38187 | . . . 4 class RefRels | |
| 3 | csymrels 38193 | . . . 4 class SymRels | |
| 4 | 2, 3 | cin 3950 | . . 3 class ( RefRels ∩ SymRels ) | 
| 5 | ctrrels 38196 | . . 3 class TrRels | |
| 6 | 4, 5 | cin 3950 | . 2 class (( RefRels ∩ SymRels ) ∩ TrRels ) | 
| 7 | 1, 6 | wceq 1540 | 1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels ) | 
| Colors of variables: wff setvar class | 
| This definition is referenced by: dfeqvrels2 38589 refrelsredund2 38634 | 
| Copyright terms: Public domain | W3C validator |