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	⊢ ( ElDisj 𝐴 ↔ Disj ( ◡ E ↾ 𝐴 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	weldisj	⊢ ElDisj 𝐴
2		cep	⊢ E
3	2	ccnv	⊢ ◡ E
4	3 0	cres	⊢ ( ◡ E ↾ 𝐴 )
5	4	wdisjALTV	⊢ Disj ( ◡ E ↾ 𝐴 )
6	1 5	wb	⊢ ( ElDisj 𝐴 ↔ Disj ( ◡ E ↾ 𝐴 ) )