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 4570 | . . . 4 ⊢ {𝐴} = {𝐴, 𝐴} | |
2 | 1 | unieqi 4839 | . . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴} |
3 | 2 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴}) |
4 | uniprg 4844 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴)) | |
5 | 4 | anidms 567 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴)) |
6 | unidm 4125 | . . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴 | |
7 | 6 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴) |
8 | 3, 5, 7 | 3eqtrd 2857 | 1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 ∪ cun 3931 {csn 4557 {cpr 4559 ∪ 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: unisn 4846 unisn3 4847 dfnfc2 4848 unisn2 5207 en2other2 9423 pmtrprfv 18510 dprdsn 19087 indistopon 21537 ordtuni 21726 cmpcld 21938 ptcmplem5 22592 cldsubg 22646 icccmplem2 23358 vmappw 25620 chsupsn 29117 xrge0tsmseq 30621 cycpm2tr 30688 qustrivr 30857 esumsnf 31222 prsiga 31289 rossros 31338 cvmscld 32417 unisnif 33283 topjoin 33610 fnejoin2 33614 bj-snmoore 34299 pibt2 34580 heiborlem8 34977 fourierdlem80 42348 |
Copyright terms: Public domain | W3C validator |