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 5115
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 5114 . 2 wff Disj 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1535 . . . . 5 class 𝑦
76, 3wcel 2105 . . . 4 wff 𝑦𝐵
87, 1, 2wrmo 3376 . . 3 wff ∃*𝑥𝐴 𝑦𝐵
98, 5wal 1534 . 2 wff 𝑦∃*𝑥𝐴 𝑦𝐵
104, 9wb 206 1 wff (Disj 𝑥𝐴 𝐵 ↔ ∀𝑦∃*𝑥𝐴 𝑦𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  dfdisj2  5116  disjss2  5117  cbvdisj  5124  cbvdisjv  5125  nfdisj1  5128  disjor  5129  disjiun  5135  cbvdisjf  32590  disjss1f  32591  disjxun0  32593  disjorf  32598  disjin  32605  disjin2  32606  disjrdx  32610  ddemeas  34216  disjeq1i  36173  disjeq12dv  36197  cbvdisjvw2  36217  cbvdisjdavw  36250  cbvdisjdavw2  36271  iccpartdisj  47361
  Copyright terms: Public domain W3C validator