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 36315.
We use subset relation S (df-ssr 36302) here to be able to define
converse reflexivity (df-cnvrefs 36327), see also the comment of df-ssr 36302.
The elements of this class are not necessarily relations (versus
df-refrels 36315).
Note the similarity of Definitions df-refs 36314, df-syms 36342 and df-trs 36372, cf. comments of dfrefrels2 36317. (Contributed by Peter Mazsa, 19-Jul-2019.) |
Ref | Expression |
---|---|
df-refs | ⊢ Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crefs 36023 | . 2 class Refs | |
2 | cid 5439 | . . . . 5 class I | |
3 | vx | . . . . . . . 8 setvar 𝑥 | |
4 | 3 | cv 1542 | . . . . . . 7 class 𝑥 |
5 | 4 | cdm 5536 | . . . . . 6 class dom 𝑥 |
6 | 4 | crn 5537 | . . . . . 6 class ran 𝑥 |
7 | 5, 6 | cxp 5534 | . . . . 5 class (dom 𝑥 × ran 𝑥) |
8 | 2, 7 | cin 3852 | . . . 4 class ( I ∩ (dom 𝑥 × ran 𝑥)) |
9 | 4, 7 | cin 3852 | . . . 4 class (𝑥 ∩ (dom 𝑥 × ran 𝑥)) |
10 | cssr 36022 | . . . 4 class S | |
11 | 8, 9, 10 | wbr 5039 | . . 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 1543 | 1 wff Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
Colors of variables: wff setvar class |
This definition is referenced by: dfrefrels2 36317 |
Copyright terms: Public domain | W3C validator |