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 4834 | . . . 4 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴)) | |
2 | elelpwi 4553 | . . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴) | |
3 | 2 | exlimiv 1927 | . . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝐴) |
4 | 1, 3 | sylbi 219 | . . 3 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 → 𝑥 ∈ 𝐴) |
5 | vsnid 4595 | . . . 4 ⊢ 𝑥 ∈ {𝑥} | |
6 | snelpwi 5328 | . . . 4 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝒫 𝐴) | |
7 | elunii 4836 | . . . 4 ⊢ ((𝑥 ∈ {𝑥} ∧ {𝑥} ∈ 𝒫 𝐴) → 𝑥 ∈ ∪ 𝒫 𝐴) | |
8 | 5, 6, 7 | sylancr 589 | . . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝒫 𝐴) |
9 | 4, 8 | impbii 211 | . 2 ⊢ (𝑥 ∈ ∪ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴) |
10 | 9 | eqriv 2818 | 1 ⊢ ∪ 𝒫 𝐴 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 398 = wceq 1533 ∃wex 1776 ∈ wcel 2110 𝒫 cpw 4538 {csn 4560 ∪ cuni 4831 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-pw 4540 df-sn 4561 df-pr 4563 df-uni 4832 |
This theorem is referenced by: univ 5335 pwtr 5337 unixpss 5677 pwexr 7481 unifpw 8821 fiuni 8886 ween 9455 fin23lem41 9768 mremre 16869 submre 16870 isacs1i 16922 eltg4i 21562 distop 21597 distopon 21599 distps 21617 ntrss2 21659 isopn3 21668 discld 21691 mretopd 21694 dishaus 21984 discmp 22000 dissnlocfin 22131 locfindis 22132 txdis 22234 xkopt 22257 xkofvcn 22286 hmphdis 22398 ustbas2 22828 vitali 24208 shsupcl 29109 shsupunss 29117 iundifdifd 30307 iundifdif 30308 dispcmp 31118 mbfmcnt 31521 omssubadd 31553 carsgval 31556 carsggect 31571 coinflipprob 31732 coinflipuniv 31734 fnemeet2 33710 bj-unirel 34338 bj-discrmoore 34397 icoreunrn 34634 ctbssinf 34681 mapdunirnN 38780 ismrcd1 39288 hbt 39723 pwelg 39912 pwsal 42594 salgenval 42600 salgenn0 42608 salexct 42611 salgencntex 42620 0ome 42805 isomennd 42807 unidmovn 42889 rrnmbl 42890 hspmbl 42905 |
Copyright terms: Public domain | W3C validator |