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 4539 | . . . 4 ⊢ {𝐴} = {𝐴, 𝐴} | |
2 | 1 | unieqi 4819 | . . 3 ⊢ ∪ {𝐴} = ∪ {𝐴, 𝐴} |
3 | 2 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = ∪ {𝐴, 𝐴}) |
4 | uniprg 4823 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴)) | |
5 | 4 | anidms 570 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴, 𝐴} = (𝐴 ∪ 𝐴)) |
6 | unidm 4052 | . . 3 ⊢ (𝐴 ∪ 𝐴) = 𝐴 | |
7 | 6 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 𝐴) = 𝐴) |
8 | 3, 5, 7 | 3eqtrd 2778 | 1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ∪ cun 3851 {csn 4526 {cpr 4528 ∪ cuni 4806 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-v 3402 df-un 3858 df-in 3860 df-ss 3870 df-sn 4527 df-pr 4529 df-uni 4807 |
This theorem is referenced by: unisn 4828 unisn3 4829 dfnfc2 4830 unisn2 5190 en2other2 9522 pmtrprfv 18712 dprdsn 19290 indistopon 21765 ordtuni 21954 cmpcld 22166 ptcmplem5 22820 cldsubg 22875 icccmplem2 23588 vmappw 25866 chsupsn 29361 xrge0tsmseq 30909 cycpm2tr 30976 qustrivr 31146 esumsnf 31615 prsiga 31682 rossros 31731 cvmscld 32819 unisnif 33883 topjoin 34210 fnejoin2 34214 bj-snmoore 34938 pibt2 35244 heiborlem8 35632 fourierdlem80 43310 |
Copyright terms: Public domain | W3C validator |