![]() |
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 38576. Alternate definitions are dfeqvrels2 38570 and dfeqvrels3 38571. (Contributed by Peter Mazsa, 7-Nov-2018.) |
Ref | Expression |
---|---|
df-eqvrels | ⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ceqvrels 38178 | . 2 class EqvRels | |
2 | crefrels 38167 | . . . 4 class RefRels | |
3 | csymrels 38173 | . . . 4 class SymRels | |
4 | 2, 3 | cin 3962 | . . 3 class ( RefRels ∩ SymRels ) |
5 | ctrrels 38176 | . . 3 class TrRels | |
6 | 4, 5 | cin 3962 | . 2 class (( RefRels ∩ SymRels ) ∩ TrRels ) |
7 | 1, 6 | wceq 1537 | 1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels ) |
Colors of variables: wff setvar class |
This definition is referenced by: dfeqvrels2 38570 refrelsredund2 38615 |
Copyright terms: Public domain | W3C validator |