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 35806
Description: Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 35807). It is used only by df-disjs 35807. (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 35356 . 2 class Disjss
2 vx . . . . . . 7 setvar 𝑥
32cv 1529 . . . . . 6 class 𝑥
43ccnv 5552 . . . . 5 class 𝑥
54ccoss 35324 . . . 4 class 𝑥
6 ccnvrefrels 35332 . . . 4 class CnvRefRels
75, 6wcel 2107 . . 3 wff 𝑥 ∈ CnvRefRels
87, 2cab 2803 . 2 class {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels }
91, 8wceq 1530 1 wff Disjss = {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels }
Colors of variables: wff setvar class
This definition is referenced by:  dfdisjs  35811
  Copyright terms: Public domain W3C validator