Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-refs | Structured version Visualization version GIF version |
Description: Define the class of all
reflexive sets. It is used only by df-refrels 35766.
We use subset relation S (df-ssr 35753) here to be able to define
converse reflexivity (df-cnvrefs 35778), see also the comment of df-ssr 35753.
The elements of this class are not necessarily relations (versus
df-refrels 35766).
Note the similarity of the definitions df-refs 35765, df-syms 35793 and df-trs 35823, cf. comments of dfrefrels2 35768. (Contributed by Peter Mazsa, 19-Jul-2019.) |
Ref | Expression |
---|---|
df-refs | ⊢ Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crefs 35472 | . 2 class Refs | |
2 | cid 5459 | . . . . 5 class I | |
3 | vx | . . . . . . . 8 setvar 𝑥 | |
4 | 3 | cv 1536 | . . . . . . 7 class 𝑥 |
5 | 4 | cdm 5555 | . . . . . 6 class dom 𝑥 |
6 | 4 | crn 5556 | . . . . . 6 class ran 𝑥 |
7 | 5, 6 | cxp 5553 | . . . . 5 class (dom 𝑥 × ran 𝑥) |
8 | 2, 7 | cin 3935 | . . . 4 class ( I ∩ (dom 𝑥 × ran 𝑥)) |
9 | 4, 7 | cin 3935 | . . . 4 class (𝑥 ∩ (dom 𝑥 × ran 𝑥)) |
10 | cssr 35471 | . . . 4 class S | |
11 | 8, 9, 10 | wbr 5066 | . . 3 wff ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥)) |
12 | 11, 3 | cab 2799 | . 2 class {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
13 | 1, 12 | wceq 1537 | 1 wff Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
Colors of variables: wff setvar class |
This definition is referenced by: dfrefrels2 35768 |
Copyright terms: Public domain | W3C validator |