![]() |
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 4402 | . . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅) | |
2 | 1 | abbii 2796 | . 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅} |
3 | df-pw 4609 | . 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅} | |
4 | df-sn 4634 | . 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅} | |
5 | 2, 3, 4 | 3eqtr4i 2764 | 1 ⊢ 𝒫 ∅ = {∅} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 {cab 2703 ⊆ wss 3947 ∅c0 4325 𝒫 cpw 4607 {csn 4633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-dif 3950 df-ss 3964 df-nul 4326 df-pw 4609 df-sn 4634 |
This theorem is referenced by: p0ex 5388 pwfi 9359 pwfiOLD 9391 ackbij1lem14 10276 fin1a2lem12 10454 0tsk 10798 hashbc 14470 incexclem 15840 sn0topon 22992 sn0cld 23085 ust0 24215 made0 27897 uhgr0vb 29008 uhgr0 29009 esumnul 33881 rankeq1o 35995 ssoninhaus 36160 sge00 45997 |
Copyright terms: Public domain | W3C validator |