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 5028
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 5027 . 2 wff Disj 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1529 . . . . 5 class 𝑦
76, 3wcel 2106 . . . 4 wff 𝑦𝐵
87, 1, 2wrmo 3145 . . 3 wff ∃*𝑥𝐴 𝑦𝐵
98, 5wal 1528 . 2 wff 𝑦∃*𝑥𝐴 𝑦𝐵
104, 9wb 207 1 wff (Disj 𝑥𝐴 𝐵 ↔ ∀𝑦∃*𝑥𝐴 𝑦𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  dfdisj2  5029  disjss2  5030  cbvdisj  5037  nfdisj1  5041  disjor  5042  disjiun  5049  cbvdisjf  30237  disjss1f  30238  disjxun0  30240  disjorf  30245  disjin  30252  disjin2  30253  disjrdx  30257  ddemeas  31382  iccpartdisj  43426
  Copyright terms: Public domain W3C validator