Definition df-disj 5134

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

This definition is referenced by:  dfdisj2  5135  disjss2  5136  cbvdisj  5143  cbvdisjv  5144  nfdisj1  5147  disjor  5148  disjiun  5154  cbvdisjf  32593  disjss1f  32594  disjxun0  32596  disjorf  32601  disjin  32608  disjin2  32609  disjrdx  32613  ddemeas  34200  disjeq1i  36156  disjeq12dv  36181  cbvdisjvw2  36201  cbvdisjdavw  36234  cbvdisjdavw2  36255  iccpartdisj  47311