![]() |
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 4933 | . 2 ⊢ (𝐴 ∈ V → ∪ {𝐴} = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ {𝐴} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∈ wcel 2099 Vcvv 3462 {csn 4633 ∪ cuni 4913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-un 3952 df-ss 3964 df-sn 4634 df-pr 4636 df-uni 4914 |
This theorem is referenced by: unisnv 4935 unidif0 5364 op1sta 6236 op2nda 6239 opswap 6240 fvssunirnOLD 6935 funfv 6989 dffv2 6997 nlim1 8519 en1bOLD 9060 tc2 9785 cflim2 10306 fin1a2lem12 10454 acsmapd 18579 ghmqusnsglem1 19274 ghmquskerlem1 19277 pmtrprfval 19485 lspuni0 20987 lss0v 20994 zrhval2 21498 indistopon 22995 refun0 23510 qtopeu 23711 hmphindis 23792 filconn 23878 ufildr 23926 cnextfres1 24063 bday1s 27861 old1 27899 madeoldsuc 27908 dimval 33495 dimvalfi 33496 locfinref 33656 pstmfval 33711 esumval 33879 esumpfinval 33908 esumpfinvalf 33909 prsiga 33964 carsggect 34152 indispconn 35062 onsucsuccmpi 36155 bj-nuliotaALT 36765 heiborlem3 37514 isomenndlem 46151 uniimaelsetpreimafv 46968 |
Copyright terms: Public domain | W3C validator |