Definition df-eldisj 39990

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 40027.

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

Assertion

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

Detailed syntax breakdown of Definition df-eldisj

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	weldisj 39419	. 2 wff ElDisj 𝐴
3		cep 5557	. . . . 5 class E
4	3	ccnv 5657	. . . 4 class ◡ E
5	4, 1	cres 5660	. . 3 class (◡ E ↾ 𝐴)
6	5	wdisjALTV 39417	. 2 wff Disj (◡ E ↾ 𝐴)
7	2, 6	wb 209	1 wff ( ElDisj 𝐴 ↔ Disj (◡ E ↾ 𝐴))

This definition is used by:  dfeldisj2  40008  dfeldisj3  40009  dfeldisj4  40010  eleldisjseldisj  40027  eldisjss  40036  eldisjeq  40039  eldisjn0elb  40043  dfmembpart2  40071  eldisjim  40085  eldisjim2  40086  eldisjn0el  40107  eldisjlem19  40111  eqvreldisj3  40127