Definition df-eldisj

Description: Define the disjoint elementhood relation predicate, i.e., the disjoint elementhood predicate. Read: the elements of A are disjoint. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is ( A e. ElDisjs <-> ElDisj A ) when A is a set, see eleldisjseldisj .

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

	Ref	Expression
Assertion	df-eldisj	$$⊢ElDisjA\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	weldisj	$$wffElDisjA$$
2		cep	$$class\mathrm{E}$$
3	2	ccnv	$$class{\mathrm{E}}^{-1}$$
4	3 0	cres	$$class\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
5	4	wdisjALTV	$$wffDisj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
6	1 5	wb	$$wff\left(ElDisjA\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\right)$$