Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-disjss Structured version   Visualization version   GIF version

Definition df-disjss 37215
Description: Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 37216). It is used only by df-disjs 37216. (Contributed by Peter Mazsa, 17-Jul-2021.)
Assertion
Ref Expression
df-disjss Disjss = {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels }

Detailed syntax breakdown of Definition df-disjss
StepHypRef Expression
1 cdisjss 36716 . 2 class Disjss
2 vx . . . . . . 7 setvar 𝑥
32cv 1541 . . . . . 6 class 𝑥
43ccnv 5636 . . . . 5 class 𝑥
54ccoss 36684 . . . 4 class 𝑥
6 ccnvrefrels 36692 . . . 4 class CnvRefRels
75, 6wcel 2107 . . 3 wff 𝑥 ∈ CnvRefRels
87, 2cab 2710 . 2 class {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels }
91, 8wceq 1542 1 wff Disjss = {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels }
Colors of variables: wff setvar class
This definition is referenced by:  dfdisjs  37220
  Copyright terms: Public domain W3C validator