| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-dju | Structured version Visualization version GIF version | ||
| Description: Disjoint union of two classes. This is a way of creating a set which contains elements corresponding to each element of 𝐴 or 𝐵, tagging each one with whether it came from 𝐴 or 𝐵. (Contributed by Jim Kingdon, 20-Jun-2022.) |
| Ref | Expression |
|---|---|
| df-dju | ⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cB | . . 3 class 𝐵 | |
| 3 | 1, 2 | cdju 9938 | . 2 class (𝐴 ⊔ 𝐵) |
| 4 | c0 4333 | . . . . 5 class ∅ | |
| 5 | 4 | csn 4626 | . . . 4 class {∅} |
| 6 | 5, 1 | cxp 5683 | . . 3 class ({∅} × 𝐴) |
| 7 | c1o 8499 | . . . . 5 class 1o | |
| 8 | 7 | csn 4626 | . . . 4 class {1o} |
| 9 | 8, 2 | cxp 5683 | . . 3 class ({1o} × 𝐵) |
| 10 | 6, 9 | cun 3949 | . 2 class (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
| 11 | 3, 10 | wceq 1540 | 1 wff (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: djueq12 9944 nfdju 9947 djuex 9948 djuexb 9949 djulcl 9950 djurcl 9951 djur 9959 djuunxp 9961 eldju2ndl 9964 eldju2ndr 9965 djuun 9966 undjudom 10208 endjudisj 10209 djuen 10210 dju1dif 10213 dju1p1e2 10214 xp2dju 10217 djucomen 10218 djuassen 10219 xpdjuen 10220 mapdjuen 10221 djudom1 10223 djuxpdom 10226 djufi 10227 djuinf 10229 infdju1 10230 ficardadju 10240 pwdjudom 10255 isfin4p1 10355 alephadd 10617 canthp1lem2 10693 |
| Copyright terms: Public domain | W3C validator |