| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > vpwex | Structured version Visualization version GIF version | ||
| Description: Power set axiom: the powerclass of a set is a set. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Revised to prove pwexg 5378 from vpwex 5377. (Revised by BJ, 10-Aug-2022.) |
| Ref | Expression |
|---|---|
| vpwex | ⊢ 𝒫 𝑥 ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-pw 4602 | . 2 ⊢ 𝒫 𝑥 = {𝑤 ∣ 𝑤 ⊆ 𝑥} | |
| 2 | axpow2 5367 | . . . . 5 ⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦) | |
| 3 | 2 | sepexi 5301 | . . . 4 ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥) |
| 4 | sseq1 4009 | . . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑤 ⊆ 𝑥 ↔ 𝑧 ⊆ 𝑥)) | |
| 5 | 4 | eqabbw 2815 | . . . . 5 ⊢ (𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥)) |
| 6 | 5 | exbii 1848 | . . . 4 ⊢ (∃𝑦 𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥)) |
| 7 | 3, 6 | mpbir 231 | . . 3 ⊢ ∃𝑦 𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} |
| 8 | 7 | issetri 3499 | . 2 ⊢ {𝑤 ∣ 𝑤 ⊆ 𝑥} ∈ V |
| 9 | 1, 8 | eqeltri 2837 | 1 ⊢ 𝒫 𝑥 ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∀wal 1538 = wceq 1540 ∃wex 1779 ∈ wcel 2108 {cab 2714 Vcvv 3480 ⊆ wss 3951 𝒫 cpw 4600 |
| 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 ax-sep 5296 ax-pow 5365 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: pwexg 5378 pwnex 7779 inf3lem7 9674 dfac8 10176 dfac13 10183 ackbij1lem8 10266 dominf 10485 numthcor 10534 dominfac 10613 intwun 10775 wunex2 10778 eltsk2g 10791 inttsk 10814 tskcard 10821 intgru 10854 gruina 10858 axgroth6 10868 ismre 17633 fnmre 17634 mreacs 17701 isacs5lem 18590 pmtrfval 19468 istopon 22918 dmtopon 22929 tgdom 22985 isfbas 23837 bj-snglex 36974 exrecfnpw 37382 pwinfi 43577 ntrrn 44135 ntrf 44136 dssmapntrcls 44141 vsetrec 49222 pgindnf 49235 |
| Copyright terms: Public domain | W3C validator |