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	|- ( Disj_ x e. A B <-> A. y E* x e. A y e. B )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		cA	|- A
2		cB	|- B
3	0 1 2	wdisj	|- Disj_ x e. A B
4		vy	|- y
5	4	cv	|- y
6	5 2	wcel	|- y e. B
7	6 0 1	wrmo	|- E* x e. A y e. B
8	7 4	wal	|- A. y E* x e. A y e. B
9	3 8	wb	|- ( Disj_ x e. A B <-> A. y E* x e. A y e. B )