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 35768
(which reveals that RefRels can not include proper
classes like I
as is elements, see comments of dfrefrels2 35768).
Another alternative definition is dfrefrels3 35769. The element of this class and the reflexive relation predicate (df-refrel 35767) are the same, that is, (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝐴 is a set, see elrefrelsrel 35774. This definition is similar to the definitions of the classes of symmetric (df-symrels 35794) and transitive (df-trrels 35824) relations. (Contributed by Peter Mazsa, 7-Jul-2019.) |
Ref | Expression |
---|---|
df-refrels | ⊢ RefRels = ( Refs ∩ Rels ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crefrels 35473 | . 2 class RefRels | |
2 | crefs 35472 | . . 3 class Refs | |
3 | crels 35470 | . . 3 class Rels | |
4 | 2, 3 | cin 3935 | . 2 class ( Refs ∩ Rels ) |
5 | 1, 4 | wceq 1537 | 1 wff RefRels = ( Refs ∩ Rels ) |
Colors of variables: wff setvar class |
This definition is referenced by: dfrefrels2 35768 |
Copyright terms: Public domain | W3C validator |