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 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		cB	⊢ 𝐵
3	0 1 2	wdisj	⊢ Disj 𝑥 ∈ 𝐴 𝐵
4		vy	⊢ 𝑦
5	4	cv	⊢ 𝑦
6	5 2	wcel	⊢ 𝑦 ∈ 𝐵
7	6 0 1	wrmo	⊢ ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
8	7 4	wal	⊢ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	3 8	wb	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )