Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > unisng | 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, 13-Aug-2002.) |
Ref | Expression |
---|---|
unisng | ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsn2 4574 | . . . 4 ⊢ {𝐴} = {𝐴, 𝐴} | |
2 | 1 | unieqi 4852 | . . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴} |
3 | 2 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴}) |
4 | uniprg 4856 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴)) | |
5 | 4 | anidms 567 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴)) |
6 | unidm 4086 | . . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴 | |
7 | 6 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴) |
8 | 3, 5, 7 | 3eqtrd 2782 | 1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2106 ∪ cun 3885 {csn 4561 {cpr 4563 ∪ cuni 4839 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-un 3892 df-in 3894 df-ss 3904 df-sn 4562 df-pr 4564 df-uni 4840 |
This theorem is referenced by: unisn 4861 unisn3 4862 dfnfc2 4863 unisn2 5236 en2other2 9765 pmtrprfv 19061 dprdsn 19639 indistopon 22151 ordtuni 22341 cmpcld 22553 ptcmplem5 23207 cldsubg 23262 icccmplem2 23986 vmappw 26265 chsupsn 29775 xrge0tsmseq 31319 cycpm2tr 31386 qustrivr 31561 esumsnf 32032 prsiga 32099 rossros 32148 cvmscld 33235 unisnif 34227 topjoin 34554 fnejoin2 34558 bj-snmoore 35284 pibt2 35588 heiborlem8 35976 nlimsuc 41048 fourierdlem80 43727 |
Copyright terms: Public domain | W3C validator |