| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pw0 | Structured version Visualization version GIF version | ||
| Description: Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
| Ref | Expression |
|---|---|
| pw0 | ⊢ 𝒫 ∅ = {∅} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ss0b 4401 | . . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅) | |
| 2 | 1 | abbii 2809 | . 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅} |
| 3 | df-pw 4602 | . 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅} | |
| 4 | df-sn 4627 | . 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅} | |
| 5 | 2, 3, 4 | 3eqtr4i 2775 | 1 ⊢ 𝒫 ∅ = {∅} |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 {cab 2714 ⊆ wss 3951 ∅c0 4333 𝒫 cpw 4600 {csn 4626 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-dif 3954 df-ss 3968 df-nul 4334 df-pw 4602 df-sn 4627 |
| This theorem is referenced by: p0ex 5384 pwfi 9357 ackbij1lem14 10272 fin1a2lem12 10451 0tsk 10795 hashbc 14492 incexclem 15872 sn0topon 23005 sn0cld 23098 ust0 24228 made0 27912 uhgr0vb 29089 uhgr0 29090 esumnul 34049 rankeq1o 36172 ssoninhaus 36449 sge00 46391 |
| Copyright terms: Public domain | W3C validator |