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 36434
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.)
Assertion
Ref Expression
df-disjss Disjss = {𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels }

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