Definition df-disj 5053

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

This definition is referenced by:  dfdisj2  5054  disjss2  5055  cbvdisj  5062  cbvdisjv  5063  nfdisj1  5066  disjor  5067  disjiun  5073  cbvdisjf  32641  disjss1f  32642  disjxun0  32644  disjorf  32649  disjin  32656  disjin2  32657  disjrdx  32661  ddemeas  34380  disjeq1i  36374  disjeq12dv  36397  cbvdisjvw2  36417  cbvdisjdavw  36450  cbvdisjdavw2  36471  iccpartdisj  47897