Definition df-disj 5079

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 5078	. 2 wff Disj 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1569	. . . . 5 class 𝑦
7	6, 3	wcel 2146	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrmo 3370	. . 3 wff ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	wal 1568	. 2 wff ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
10	4, 9	wb 209	1 wff (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)

This definition is used by:  dfdisj2  5080  disjss2  5081  cbvdisj  5088  cbvdisjv  5089  nfdisj1  5092  disjor  5093  disjiun  5099  cbvdisjf  32963  disjss1f  32964  disjxun0  32966  disjorf  32971  disjin  32978  disjin2  32979  disjrdx  32983  ddemeas  34667  disjeq1i  36737  disjeq12dv  36760  cbvdisjvw2  36780  cbvdisjdavw  36813  cbvdisjdavw2  36834  iccpartdisj  48219