| 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 38512.
We use subset relation S (df-ssr 38499) here to be able to define
converse reflexivity (df-cnvrefs 38526), see also the comment of df-ssr 38499.
The elements of this class are not necessarily relations (versus
df-refrels 38512).
Note the similarity of Definitions df-refs 38511, df-syms 38543 and df-trs 38573, cf. comments of dfrefrels2 38514. (Contributed by Peter Mazsa, 19-Jul-2019.) |
| Ref | Expression |
|---|---|
| df-refs | ⊢ Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | crefs 38186 | . 2 class Refs | |
| 2 | cid 5577 | . . . . 5 class I | |
| 3 | vx | . . . . . . . 8 setvar 𝑥 | |
| 4 | 3 | cv 1539 | . . . . . . 7 class 𝑥 |
| 5 | 4 | cdm 5685 | . . . . . 6 class dom 𝑥 |
| 6 | 4 | crn 5686 | . . . . . 6 class ran 𝑥 |
| 7 | 5, 6 | cxp 5683 | . . . . 5 class (dom 𝑥 × ran 𝑥) |
| 8 | 2, 7 | cin 3950 | . . . 4 class ( I ∩ (dom 𝑥 × ran 𝑥)) |
| 9 | 4, 7 | cin 3950 | . . . 4 class (𝑥 ∩ (dom 𝑥 × ran 𝑥)) |
| 10 | cssr 38185 | . . . 4 class S | |
| 11 | 8, 9, 10 | wbr 5143 | . . 3 wff ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥)) |
| 12 | 11, 3 | cab 2714 | . 2 class {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
| 13 | 1, 12 | wceq 1540 | 1 wff Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfrefrels2 38514 |
| Copyright terms: Public domain | W3C validator |