Definition df-disj 5059

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

This definition is referenced by:  dfdisj2  5060  disjss2  5061  cbvdisj  5068  cbvdisjv  5069  nfdisj1  5072  disjor  5073  disjiun  5079  cbvdisjf  32549  disjss1f  32550  disjxun0  32552  disjorf  32557  disjin  32564  disjin2  32565  disjrdx  32569  ddemeas  34247  disjeq1i  36232  disjeq12dv  36255  cbvdisjvw2  36275  cbvdisjdavw  36308  cbvdisjdavw2  36329  iccpartdisj  47474