Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-disjss | Structured version Visualization version GIF version |
Description: Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 36435). It is used only by df-disjs 36435. (Contributed by Peter Mazsa, 17-Jul-2021.) |
Ref | Expression |
---|---|
df-disjss | ⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdisjss 35985 | . 2 class Disjss | |
2 | vx | . . . . . . 7 setvar 𝑥 | |
3 | 2 | cv 1541 | . . . . . 6 class 𝑥 |
4 | 3 | ccnv 5525 | . . . . 5 class ◡𝑥 |
5 | 4 | ccoss 35953 | . . . 4 class ≀ ◡𝑥 |
6 | ccnvrefrels 35961 | . . . 4 class CnvRefRels | |
7 | 5, 6 | wcel 2113 | . . 3 wff ≀ ◡𝑥 ∈ CnvRefRels |
8 | 7, 2 | cab 2716 | . 2 class {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels } |
9 | 1, 8 | wceq 1542 | 1 wff Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels } |
Colors of variables: wff setvar class |
This definition is referenced by: dfdisjs 36439 |
Copyright terms: Public domain | W3C validator |