Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > unidm | Structured version Visualization version GIF version |
Description: Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
unidm | ⊢ (𝐴 ∪ 𝐴) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oridm 535 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐴) ↔ 𝑥 ∈ 𝐴) | |
2 | 1 | uneqri 3717 | 1 ⊢ (𝐴 ∪ 𝐴) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∈ wcel 1977 ∪ cun 3538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 |
This theorem is referenced by: unundi 3736 unundir 3737 uneqin 3837 difabs 3851 undifabs 3997 dfif5 4052 dfsn2 4138 diftpsn3OLD 4274 unisn 4387 dfdm2 5584 unixpid 5587 fun2 5980 resasplit 5987 xpider 7705 pm54.43 8709 dmtrclfv 13607 lefld 17049 symg2bas 17641 gsumzaddlem 18144 pwssplit1 18880 plyun0 23757 constr3trllem3 26180 carsgsigalem 29704 sseqf 29781 probun 29808 filnetlem3 31545 mapfzcons 36297 diophin 36354 pwssplit4 36677 fiuneneq 36794 rclexi 36941 rtrclex 36943 dfrtrcl5 36955 dfrcl2 36985 iunrelexp0 37013 relexpiidm 37015 corclrcl 37018 relexp01min 37024 cotrcltrcl 37036 clsk1indlem3 37361 compne 37665 fiiuncl 38259 fzopredsuc 39946 1wlkp1 40890 |
Copyright terms: Public domain | W3C validator |