![]() |
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 37376.
We use subset relation S (df-ssr 37363) here to be able to define
converse reflexivity (df-cnvrefs 37390), see also the comment of df-ssr 37363.
The elements of this class are not necessarily relations (versus
df-refrels 37376).
Note the similarity of Definitions df-refs 37375, df-syms 37407 and df-trs 37437, cf. comments of dfrefrels2 37378. (Contributed by Peter Mazsa, 19-Jul-2019.) |
Ref | Expression |
---|---|
df-refs | ⊢ Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crefs 37042 | . 2 class Refs | |
2 | cid 5573 | . . . . 5 class I | |
3 | vx | . . . . . . . 8 setvar 𝑥 | |
4 | 3 | cv 1540 | . . . . . . 7 class 𝑥 |
5 | 4 | cdm 5676 | . . . . . 6 class dom 𝑥 |
6 | 4 | crn 5677 | . . . . . 6 class ran 𝑥 |
7 | 5, 6 | cxp 5674 | . . . . 5 class (dom 𝑥 × ran 𝑥) |
8 | 2, 7 | cin 3947 | . . . 4 class ( I ∩ (dom 𝑥 × ran 𝑥)) |
9 | 4, 7 | cin 3947 | . . . 4 class (𝑥 ∩ (dom 𝑥 × ran 𝑥)) |
10 | cssr 37041 | . . . 4 class S | |
11 | 8, 9, 10 | wbr 5148 | . . 3 wff ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥)) |
12 | 11, 3 | cab 2709 | . 2 class {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
13 | 1, 12 | wceq 1541 | 1 wff Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))} |
Colors of variables: wff setvar class |
This definition is referenced by: dfrefrels2 37378 |
Copyright terms: Public domain | W3C validator |