MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-disj Structured version   Visualization version   GIF version

Definition df-disj 4996
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
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
41, 2, 3wdisj 4995 . 2 wff Disj 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1541 . . . . 5 class 𝑦
76, 3wcel 2114 . . . 4 wff 𝑦𝐵
87, 1, 2wrmo 3056 . . 3 wff ∃*𝑥𝐴 𝑦𝐵
98, 5wal 1540 . 2 wff 𝑦∃*𝑥𝐴 𝑦𝐵
104, 9wb 209 1 wff (Disj 𝑥𝐴 𝐵 ↔ ∀𝑦∃*𝑥𝐴 𝑦𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  dfdisj2  4997  disjss2  4998  cbvdisj  5005  nfdisj1  5009  disjor  5010  disjiun  5017  cbvdisjf  30484  disjss1f  30485  disjxun0  30487  disjorf  30492  disjin  30499  disjin2  30500  disjrdx  30504  ddemeas  31774  iccpartdisj  44443
  Copyright terms: Public domain W3C validator