![]() |
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 | unisn.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | unisng 4760 | . 2 ⊢ (𝐴 ∈ V → ∪ {𝐴} = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ {𝐴} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 ∈ wcel 2081 Vcvv 3437 {csn 4472 ∪ cuni 4745 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-rex 3111 df-v 3439 df-un 3864 df-sn 4473 df-pr 4475 df-uni 4746 |
This theorem is referenced by: uniintsn 4819 unidif0 5151 op1sta 5957 op2nda 5960 opswap 5961 unisuc 6142 uniabio 6199 fvssunirn 6567 opabiotafun 6611 funfv 6617 dffv2 6623 onuninsuci 7411 en1b 8425 tc2 9030 cflim2 9531 fin1a2lem10 9677 fin1a2lem12 9679 incexclem 15024 acsmapd 17617 pmtrprfval 18346 sylow2a 18474 lspuni0 19472 lss0v 19478 zrhval2 20338 indistopon 21293 refun0 21807 1stckgenlem 21845 qtopeu 22008 hmphindis 22089 filconn 22175 ufildr 22223 alexsubALTlem3 22341 ptcmplem2 22345 cnextfres1 22360 icccmplem1 23113 unidifsnel 29984 unidifsnne 29985 disjabrex 30022 disjabrexf 30023 dimval 30605 dimvalfi 30606 locfinref 30722 pstmfval 30753 esumval 30922 esumpfinval 30951 esumpfinvalf 30952 prsiga 31007 fiunelcarsg 31191 carsgclctunlem1 31192 carsggect 31193 indispconn 32089 fobigcup 32970 onsucsuccmpi 33400 bj-nuliotaALT 33949 mbfresfi 34469 heiborlem3 34623 isomenndlem 42354 |
Copyright terms: Public domain | W3C validator |