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 1539	. . . . 5 class 𝑦
7	6, 3	wcel 2109	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrmo 3355	. . 3 wff ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	wal 1538	. 2 wff ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
10	4, 9	wb 206	1 wff (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)

This definition is referenced by:  dfdisj2  5079  disjss2  5080  cbvdisj  5087  cbvdisjv  5088  nfdisj1  5091  disjor  5092  disjiun  5098  cbvdisjf  32507  disjss1f  32508  disjxun0  32510  disjorf  32515  disjin  32522  disjin2  32523  disjrdx  32527  ddemeas  34233  disjeq1i  36187  disjeq12dv  36210  cbvdisjvw2  36230  cbvdisjdavw  36263  cbvdisjdavw2  36284  iccpartdisj  47442