![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-disj | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-disj | ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . 3 setvar 𝑥 | |
2 | cA | . . 3 class 𝐴 | |
3 | cB | . . 3 class 𝐵 | |
4 | 1, 2, 3 | wdisj 5114 | . 2 wff Disj 𝑥 ∈ 𝐴 𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1535 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2105 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wrmo 3376 | . . 3 wff ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
9 | 8, 5 | wal 1534 | . 2 wff ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
10 | 4, 9 | wb 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 |