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 5114
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 5113 . 2 wff Disj 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1539 . . . . 5 class 𝑦
76, 3wcel 2105 . . . 4 wff 𝑦𝐵
87, 1, 2wrmo 3374 . . 3 wff ∃*𝑥𝐴 𝑦𝐵
98, 5wal 1538 . 2 wff 𝑦∃*𝑥𝐴 𝑦𝐵
104, 9wb 205 1 wff (Disj 𝑥𝐴 𝐵 ↔ ∀𝑦∃*𝑥𝐴 𝑦𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  dfdisj2  5115  disjss2  5116  cbvdisj  5123  nfdisj1  5127  disjor  5128  disjiun  5135  cbvdisjf  32234  disjss1f  32235  disjxun0  32237  disjorf  32242  disjin  32249  disjin2  32250  disjrdx  32254  ddemeas  33697  iccpartdisj  46563
  Copyright terms: Public domain W3C validator