![]() |
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 37085. Alternate definitions are dfeqvrels2 37079 and dfeqvrels3 37080. (Contributed by Peter Mazsa, 7-Nov-2018.) |
Ref | Expression |
---|---|
df-eqvrels | ⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ceqvrels 36679 | . 2 class EqvRels | |
2 | crefrels 36668 | . . . 4 class RefRels | |
3 | csymrels 36674 | . . . 4 class SymRels | |
4 | 2, 3 | cin 3914 | . . 3 class ( RefRels ∩ SymRels ) |
5 | ctrrels 36677 | . . 3 class TrRels | |
6 | 4, 5 | cin 3914 | . 2 class (( RefRels ∩ SymRels ) ∩ TrRels ) |
7 | 1, 6 | wceq 1542 | 1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels ) |
Colors of variables: wff setvar class |
This definition is referenced by: dfeqvrels2 37079 refrelsredund2 37124 |
Copyright terms: Public domain | W3C validator |