Definition df-disj 5066

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 5065	. 2 wff Disj 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1540	. . . . 5 class 𝑦
7	6, 3	wcel 2113	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrmo 3349	. . 3 wff ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	wal 1539	. 2 wff ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
10	4, 9	wb 206	1 wff (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)

This definition is referenced by:  dfdisj2  5067  disjss2  5068  cbvdisj  5075  cbvdisjv  5076  nfdisj1  5079  disjor  5080  disjiun  5086  cbvdisjf  32646  disjss1f  32647  disjxun0  32649  disjorf  32654  disjin  32661  disjin2  32662  disjrdx  32666  ddemeas  34393  disjeq1i  36386  disjeq12dv  36409  cbvdisjvw2  36429  cbvdisjdavw  36462  cbvdisjdavw2  36483  iccpartdisj  47683