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 5041
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 5040 . 2 wff Disj 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1538 . . . . 5 class 𝑦
76, 3wcel 2107 . . . 4 wff 𝑦𝐵
87, 1, 2wrmo 3068 . . 3 wff ∃*𝑥𝐴 𝑦𝐵
98, 5wal 1537 . 2 wff 𝑦∃*𝑥𝐴 𝑦𝐵
104, 9wb 205 1 wff (Disj 𝑥𝐴 𝐵 ↔ ∀𝑦∃*𝑥𝐴 𝑦𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  dfdisj2  5042  disjss2  5043  cbvdisj  5050  nfdisj1  5054  disjor  5055  disjiun  5062  cbvdisjf  30919  disjss1f  30920  disjxun0  30922  disjorf  30927  disjin  30934  disjin2  30935  disjrdx  30939  ddemeas  32213  iccpartdisj  44900
  Copyright terms: Public domain W3C validator