Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > unisn | Structured version Visualization version GIF version |
Description: A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
unisn.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
unisn | ⊢ ∪ {𝐴} = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsn2 4138 | . . 3 ⊢ {𝐴} = {𝐴, 𝐴} | |
2 | 1 | unieqi 4381 | . 2 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴} |
3 | unisn.1 | . . 3 ⊢ 𝐴 ∈ V | |
4 | 3, 3 | unipr 4385 | . 2 ⊢ ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴) |
5 | unidm 3718 | . 2 ⊢ (𝐴 ∪ 𝐴) = 𝐴 | |
6 | 2, 4, 5 | 3eqtri 2636 | 1 ⊢ ∪ {𝐴} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∈ wcel 1977 Vcvv 3173 ∪ cun 3538 {csn 4125 {cpr 4127 ∪ cuni 4372 |
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-rex 2902 df-v 3175 df-un 3545 df-sn 4126 df-pr 4128 df-uni 4373 |
This theorem is referenced by: unisng 4388 uniintsn 4449 unidif0 4764 op1sta 5535 op2nda 5538 opswap 5540 unisuc 5718 uniabio 5778 fvssunirn 6127 opabiotafun 6169 funfv 6175 dffv2 6181 onuninsuci 6932 en1b 7910 tc2 8501 cflim2 8968 fin1a2lem10 9114 fin1a2lem12 9116 incexclem 14407 acsmapd 17001 pmtrprfval 17730 sylow2a 17857 lspuni0 18831 lss0v 18837 zrhval2 19676 indistopon 20615 refun0 21128 1stckgenlem 21166 qtopeu 21329 hmphindis 21410 filcon 21497 ufildr 21545 alexsubALTlem3 21663 ptcmplem2 21667 cnextfres1 21682 icccmplem1 22433 disjabrex 28777 disjabrexf 28778 locfinref 29236 pstmfval 29267 esumval 29435 esumpfinval 29464 esumpfinvalf 29465 prsiga 29521 fiunelcarsg 29705 carsgclctunlem1 29706 carsggect 29707 indispcon 30470 fobigcup 31177 onsucsuccmpi 31612 bj-nuliotaALT 32211 mbfresfi 32626 heiborlem3 32782 prsal 39214 isomenndlem 39420 |
Copyright terms: Public domain | W3C validator |