| 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 5110 | . 2 wff Disj 𝑥 ∈ 𝐴 𝐵 |
| 5 | vy | . . . . . 6 setvar 𝑦 | |
| 6 | 5 | cv 1539 | . . . . 5 class 𝑦 |
| 7 | 6, 3 | wcel 2108 | . . . 4 wff 𝑦 ∈ 𝐵 |
| 8 | 7, 1, 2 | wrmo 3379 | . . 3 wff ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
| 9 | 8, 5 | wal 1538 | . 2 wff ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
| 10 | 4, 9 | wb 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 |