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 901 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐴) ↔ 𝑥 ∈ 𝐴) | |
2 | 1 | uneqri 4126 | 1 ⊢ (𝐴 ∪ 𝐴) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∈ wcel 2110 ∪ cun 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-un 3940 |
This theorem is referenced by: unundi 4145 unundir 4146 uneqin 4254 difabs 4267 undifabs 4425 dfif5 4482 dfsn2 4579 unisng 4856 dfdm2 6131 unixpid 6134 fun2 6540 resasplit 6547 xpider 8367 pm54.43 9428 dmtrclfv 14377 lefld 17835 symg2bas 18520 gsumzaddlem 19040 pwssplit1 19830 plyun0 24786 wlkp1 27462 cycpmco2f1 30766 carsgsigalem 31573 sseqf 31650 probun 31677 nodenselem5 33192 filnetlem3 33728 pibt2 34697 mapfzcons 39311 diophin 39367 pwssplit4 39687 fiuneneq 39795 rclexi 39973 rtrclex 39975 dfrtrcl5 39987 dfrcl2 40017 iunrelexp0 40045 relexpiidm 40047 corclrcl 40050 relexp01min 40056 cotrcltrcl 40068 clsk1indlem3 40391 fiiuncl 41325 fzopredsuc 43522 |
Copyright terms: Public domain | W3C validator |