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 35977). It is used only by df-disjs 35977. (Contributed by Peter Mazsa, 17-Jul-2021.) |
Ref | Expression |
---|---|
df-disjss | ⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdisjss 35525 | . 2 class Disjss | |
2 | vx | . . . . . . 7 setvar 𝑥 | |
3 | 2 | cv 1535 | . . . . . 6 class 𝑥 |
4 | 3 | ccnv 5547 | . . . . 5 class ◡𝑥 |
5 | 4 | ccoss 35493 | . . . 4 class ≀ ◡𝑥 |
6 | ccnvrefrels 35501 | . . . 4 class CnvRefRels | |
7 | 5, 6 | wcel 2113 | . . 3 wff ≀ ◡𝑥 ∈ CnvRefRels |
8 | 7, 2 | cab 2798 | . 2 class {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels } |
9 | 1, 8 | wceq 1536 | 1 wff Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels } |
Colors of variables: wff setvar class |
This definition is referenced by: dfdisjs 35981 |
Copyright terms: Public domain | W3C validator |