Definition df-disj 5040

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

Assertion

Ref	Expression
df-disj	⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑦,𝐵

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-disj

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		cA	. . 3 class 𝐴
3		cB	. . 3 class 𝐵
4	1, 2, 3	wdisj 5039	. 2 wff Disj 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1546	. . . . 5 class 𝑦
7	6, 3	wcel 2119	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrmo 3343	. . 3 wff ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	wal 1545	. 2 wff ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
10	4, 9	wb 207	1 wff (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)

This definition is referenced by:  dfdisj2  5041  disjss2  5042  cbvdisj  5049  cbvdisjv  5050  nfdisj1  5053  disjor  5054  disjiun  5060  cbvdisjf  32660  disjss1f  32661  disjxun0  32663  disjorf  32668  disjin  32675  disjin2  32676  disjrdx  32680  ddemeas  34420  disjeq1i  36420  disjeq12dv  36443  cbvdisjvw2  36463  cbvdisjdavw  36496  cbvdisjdavw2  36517  iccpartdisj  47912