![]() |
Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-refrels | Structured version Visualization version GIF version |
Description: Define the class of
reflexive relations. This is practically dfrefrels2 37383
(which reveals that RefRels can not include proper
classes like I
as is elements, see comments of dfrefrels2 37383).
Another alternative definition is dfrefrels3 37384. The element of this class and the reflexive relation predicate (df-refrel 37382) are the same, that is, (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝐴 is a set, see elrefrelsrel 37390. This definition is similar to the definitions of the classes of symmetric (df-symrels 37413) and transitive (df-trrels 37443) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
Ref | Expression |
---|---|
df-refrels | ⊢ RefRels = ( Refs ∩ Rels ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crefrels 37048 | . 2 class RefRels | |
2 | crefs 37047 | . . 3 class Refs | |
3 | crels 37045 | . . 3 class Rels | |
4 | 2, 3 | cin 3948 | . 2 class ( Refs ∩ Rels ) |
5 | 1, 4 | wceq 1542 | 1 wff RefRels = ( Refs ∩ Rels ) |
Colors of variables: wff setvar class |
This definition is referenced by: dfrefrels2 37383 |
Copyright terms: Public domain | W3C validator |