![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > unipw | Structured version Visualization version GIF version |
Description: A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) (Proof shortened by Alan Sare, 28-Dec-2008.) |
Ref | Expression |
---|---|
unipw | ⊢ ∪ 𝒫 𝐴 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluni 4912 | . . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴)) | |
2 | elelpwi 4613 | . . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴) | |
3 | 2 | exlimiv 1934 | . . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴) |
4 | 1, 3 | sylbi 216 | . . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴) |
5 | vsnid 4666 | . . . 4 ⊢ 𝑥 ∈ {𝑥} | |
6 | snelpwi 5444 | . . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴) | |
7 | elunii 4914 | . . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴) | |
8 | 5, 6, 7 | sylancr 588 | . . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴) |
9 | 4, 8 | impbii 208 | . 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴) |
10 | 9 | eqriv 2730 | 1 ⊢ ∪ 𝒫 𝐴 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 𝒫 cpw 4603 {csn 4629 ∪ cuni 4909 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5300 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3954 df-in 3956 df-ss 3966 df-pw 4605 df-sn 4630 df-pr 4632 df-uni 4910 |
This theorem is referenced by: univ 5452 pwtr 5453 unixpss 5811 pwexr 7752 unifpw 9355 fiuni 9423 ween 10030 fin23lem41 10347 mremre 17548 submre 17549 isacs1i 17601 eltg4i 22463 distop 22498 distopon 22500 distps 22519 ntrss2 22561 isopn3 22570 discld 22593 mretopd 22596 dishaus 22886 discmp 22902 dissnlocfin 23033 locfindis 23034 txdis 23136 xkopt 23159 xkofvcn 23188 hmphdis 23300 ustbas2 23730 vitali 25130 shsupcl 30591 shsupunss 30599 iundifdifd 31793 iundifdif 31794 dispcmp 32839 mbfmcnt 33267 omssubadd 33299 carsgval 33302 carsggect 33317 coinflipprob 33478 coinflipuniv 33480 fnemeet2 35252 bj-unirel 35932 bj-discrmoore 35992 icoreunrn 36240 ctbssinf 36287 mapdunirnN 40521 ismrcd1 41436 hbt 41872 pwelg 42311 pwsal 45031 salgenval 45037 salgenn0 45047 salexct 45050 salgencntex 45059 0ome 45245 isomennd 45247 unidmovn 45329 rrnmbl 45330 hspmbl 45345 |
Copyright terms: Public domain | W3C validator |