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 5111
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 5110 . 2 wff Disj 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1539 . . . . 5 class 𝑦
76, 3wcel 2108 . . . 4 wff 𝑦𝐵
87, 1, 2wrmo 3379 . . 3 wff ∃*𝑥𝐴 𝑦𝐵
98, 5wal 1538 . 2 wff 𝑦∃*𝑥𝐴 𝑦𝐵
104, 9wb 206 1 wff (Disj 𝑥𝐴 𝐵 ↔ ∀𝑦∃*𝑥𝐴 𝑦𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  dfdisj2  5112  disjss2  5113  cbvdisj  5120  cbvdisjv  5121  nfdisj1  5124  disjor  5125  disjiun  5131  cbvdisjf  32584  disjss1f  32585  disjxun0  32587  disjorf  32592  disjin  32599  disjin2  32600  disjrdx  32604  ddemeas  34237  disjeq1i  36193  disjeq12dv  36216  cbvdisjvw2  36236  cbvdisjdavw  36269  cbvdisjdavw2  36290  iccpartdisj  47424
  Copyright terms: Public domain W3C validator