Definition df-disj

Description: A collection of classes B ( x ) is disjoint when for each element y , it is in B ( x ) for at most one x . (Contributed by Mario Carneiro, 14-Nov-2016) (Revised by NM, 16-Jun-2017)

	Ref	Expression
Assertion	df-disj	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall y{\exists }^{*}x\in Ay\in B$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		cB	$$classB$$
3	0 1 2	wdisj	$$wff\underset{x\in A}{Disj}B$$
4		vy	$$setvary$$
5	4	cv	$$setvary$$
6	5 2	wcel	$$wffy\in B$$
7	6 0 1	wrmo	$$wff{\exists }^{*}x\in Ay\in B$$
8	7 4	wal	$$wff\forall y{\exists }^{*}x\in Ay\in B$$
9	3 8	wb	$$wff\left(\underset{x\in A}{Disj}B\leftrightarrow \forall y{\exists }^{*}x\in Ay\in B\right)$$