Definition df-disj 5078

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

This definition is referenced by:  dfdisj2  5079  disjss2  5080  cbvdisj  5087  cbvdisjv  5088  nfdisj1  5091  disjor  5092  disjiun  5098  cbvdisjf  32853  disjss1f  32854  disjxun0  32856  disjorf  32861  disjin  32868  disjin2  32869  disjrdx  32873  ddemeas  34567  disjeq1i  36589  disjeq12dv  36612  cbvdisjvw2  36632  cbvdisjdavw  36665  cbvdisjdavw2  36686  iccpartdisj  48068