![]() |
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 4277 | . . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅) | |
2 | 1 | abbii 2863 | . 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅} |
3 | df-pw 4461 | . 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅} | |
4 | df-sn 4479 | . 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅} | |
5 | 2, 3, 4 | 3eqtr4i 2831 | 1 ⊢ 𝒫 ∅ = {∅} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1525 {cab 2777 ⊆ wss 3865 ∅c0 4217 𝒫 cpw 4459 {csn 4478 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-dif 3868 df-in 3872 df-ss 3880 df-nul 4218 df-pw 4461 df-sn 4479 |
This theorem is referenced by: p0ex 5182 pwfi 8672 ackbij1lem14 9508 fin1a2lem12 9686 0tsk 10030 hashbc 13663 incexclem 15028 sn0topon 21294 sn0cld 21386 ust0 22515 uhgr0vb 26544 uhgr0 26545 esumnul 30920 rankeq1o 33243 ssoninhaus 33407 sge00 42222 |
Copyright terms: Public domain | W3C validator |