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 | sneq 4135 | . . . 4 ⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴}) | |
2 | 1 | unieqd 4382 | . . 3 ⊢ (𝑥 = 𝐴 → ∪ {𝑥} = ∪ {𝐴}) |
3 | id 22 | . . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | |
4 | 2, 3 | eqeq12d 2625 | . 2 ⊢ (𝑥 = 𝐴 → (∪ {𝑥} = 𝑥 ↔ ∪ {𝐴} = 𝐴)) |
5 | vex 3176 | . . 3 ⊢ 𝑥 ∈ V | |
6 | 5 | unisn 4387 | . 2 ⊢ ∪ {𝑥} = 𝑥 |
7 | 4, 6 | vtoclg 3239 | 1 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 {csn 4125 ∪ cuni 4372 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-v 3175 df-un 3545 df-sn 4126 df-pr 4128 df-uni 4373 |
This theorem is referenced by: unisn3 4389 dfnfc2 4390 dfnfc2OLD 4391 unisn2 4722 en2other2 8715 pmtrprfv 17696 dprdsn 18258 indistopon 20615 ordtuni 20804 cmpcld 21015 ptcmplem5 21670 cldsubg 21724 icccmplem2 22434 vmappw 24642 chsupsn 27656 xrge0tsmseq 29118 esumsnf 29453 prsiga 29521 rossros 29570 cvmscld 30509 unisnif 31202 topjoin 31530 fnejoin2 31534 heiborlem8 32787 fourierdlem80 39079 |
Copyright terms: Public domain | W3C validator |