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 4845 | . 2 ⊢ (𝐴 ∈ V → ∪ {𝐴} = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ {𝐴} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∈ wcel 2105 Vcvv 3492 {csn 4557 ∪ cuni 4830 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rex 3141 df-v 3494 df-un 3938 df-sn 4558 df-pr 4560 df-uni 4831 |
This theorem is referenced by: uniintsn 4904 unidif0 5251 op1sta 6075 op2nda 6078 opswap 6079 unisuc 6260 uniabio 6321 fvssunirn 6692 opabiotafun 6737 funfv 6743 dffv2 6749 onuninsuci 7544 en1b 8565 tc2 9172 cflim2 9673 fin1a2lem10 9819 fin1a2lem12 9821 incexclem 15179 acsmapd 17776 pmtrprfval 18544 sylow2a 18673 lspuni0 19711 lss0v 19717 zrhval2 20584 indistopon 21537 refun0 22051 1stckgenlem 22089 qtopeu 22252 hmphindis 22333 filconn 22419 ufildr 22467 alexsubALTlem3 22585 ptcmplem2 22589 cnextfres1 22604 icccmplem1 23357 unidifsnel 30222 unidifsnne 30223 disjabrex 30260 disjabrexf 30261 dimval 30900 dimvalfi 30901 locfinref 31004 pstmfval 31035 esumval 31204 esumpfinval 31233 esumpfinvalf 31234 prsiga 31289 fiunelcarsg 31473 carsgclctunlem1 31474 carsggect 31475 indispconn 32378 fobigcup 33258 onsucsuccmpi 33688 bj-nuliotaALT 34245 mbfresfi 34819 heiborlem3 34972 isomenndlem 42689 uniimaelsetpreimafv 43433 |
Copyright terms: Public domain | W3C validator |