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