| 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 905 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐴) ↔ 𝑥 ∈ 𝐴) | |
| 2 | 1 | uneqri 4156 | 1 ⊢ (𝐴 ∪ 𝐴) = 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2108 ∪ cun 3949 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 |
| This theorem is referenced by: unundi 4176 unundir 4177 uneqin 4289 difabs 4303 undifabs 4478 dfif5 4542 dfsn2 4639 unisng 4925 dfdm2 6301 unixpid 6304 f1imadifssran 6652 fun2 6771 resasplit 6778 xpider 8828 pm54.43 10041 dmtrclfv 15057 lefld 18637 symg2bas 19410 gsumzaddlem 19939 pwssplit1 21058 plyun0 26236 nodenselem5 27733 addsproplem6 28007 mulsproplem12 28153 mulsproplem13 28154 mulsproplem14 28155 n0scut 28338 1p1e2s 28400 nohalf 28407 halfcut 28416 readdscl 28431 remulscl 28434 wlkp1 29699 cycpmco2f1 33144 carsgsigalem 34317 sseqf 34394 probun 34421 filnetlem3 36381 pibt2 37418 metakunt21 42226 metakunt22 42227 metakunt24 42229 mapfzcons 42727 diophin 42783 pwssplit4 43101 fiuneneq 43204 rclexi 43628 rtrclex 43630 dfrtrcl5 43642 dfrcl2 43687 iunrelexp0 43715 relexpiidm 43717 corclrcl 43720 relexp01min 43726 cotrcltrcl 43738 clsk1indlem3 44056 fiiuncl 45070 fzopredsuc 47335 |
| Copyright terms: Public domain | W3C validator |