Definition df-disj 5065

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 5064	. 2 wff Disj 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1558	. . . . 5 class 𝑦
7	6, 3	wcel 2141	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrmo 3365	. . 3 wff ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	wal 1557	. 2 wff ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
10	4, 9	wb 208	1 wff (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)

This definition is referenced by:  dfdisj2  5066  disjss2  5067  cbvdisj  5074  cbvdisjv  5075  nfdisj1  5078  disjor  5079  disjiun  5085  cbvdisjf  32731  disjss1f  32732  disjxun0  32734  disjorf  32739  disjin  32746  disjin2  32747  disjrdx  32751  ddemeas  34494  disjeq1i  36513  disjeq12dv  36536  cbvdisjvw2  36556  cbvdisjdavw  36589  cbvdisjdavw2  36610  iccpartdisj  48004