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

Definition df-eldisj 37219
Description: Define the disjoint element relation predicate, i.e., the disjoint elementhood predicate. Read: the elements of 𝐴 are disjoint. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set, see eleldisjseldisj 37241.

As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt 37384 with dfeldisj5 37233. See also the comments of dfmembpart2 37282 and of df-parts 37277. (Contributed by Peter Mazsa, 17-Jul-2021.)

Assertion
Ref Expression
df-eldisj ( ElDisj 𝐴 ↔ Disj ( E ↾ 𝐴))

Detailed syntax breakdown of Definition df-eldisj
StepHypRef Expression
1 cA . . 3 class 𝐴
21weldisj 36720 . 2 wff ElDisj 𝐴
3 cep 5540 . . . . 5 class E
43ccnv 5636 . . . 4 class E
54, 1cres 5639 . . 3 class ( E ↾ 𝐴)
65wdisjALTV 36718 . 2 wff Disj ( E ↾ 𝐴)
72, 6wb 205 1 wff ( ElDisj 𝐴 ↔ Disj ( E ↾ 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  dfeldisj2  37230  dfeldisj3  37231  dfeldisj4  37232  eleldisjseldisj  37241  eldisjss  37250  eldisjeq  37253  eldisjn0elb  37257  dfmembpart2  37282  eldisjim  37296  eldisjim2  37297  eldisjn0el  37318  eldisjlem19  37322  eqvreldisj3  37338
  Copyright terms: Public domain W3C validator