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 36471. Alternate definitions are dfeqvrels2 36465 and dfeqvrels3 36466. (Contributed by Peter Mazsa, 7-Nov-2018.) |
Ref | Expression |
---|---|
df-eqvrels | ⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ceqvrels 36113 | . 2 class EqvRels | |
2 | crefrels 36102 | . . . 4 class RefRels | |
3 | csymrels 36108 | . . . 4 class SymRels | |
4 | 2, 3 | cin 3880 | . . 3 class ( RefRels ∩ SymRels ) |
5 | ctrrels 36111 | . . 3 class TrRels | |
6 | 4, 5 | cin 3880 | . 2 class (( RefRels ∩ SymRels ) ∩ TrRels ) |
7 | 1, 6 | wceq 1543 | 1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels ) |
Colors of variables: wff setvar class |
This definition is referenced by: dfeqvrels2 36465 refrelsredund2 36510 |
Copyright terms: Public domain | W3C validator |