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 5242 from vpwex 5241. (Revised by BJ, 10-Aug-2022.) |
Ref | Expression |
---|---|
vpwex | ⊢ 𝒫 𝑥 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-pw 4487 | . 2 ⊢ 𝒫 𝑥 = {𝑤 ∣ 𝑤 ⊆ 𝑥} | |
2 | axpow2 5231 | . . . . 5 ⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦) | |
3 | 2 | bm1.3ii 5167 | . . . 4 ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥) |
4 | sseq1 3900 | . . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑤 ⊆ 𝑥 ↔ 𝑧 ⊆ 𝑥)) | |
5 | 4 | abeq2w 2810 | . . . . 5 ⊢ (𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥)) |
6 | 5 | exbii 1854 | . . . 4 ⊢ (∃𝑦 𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥)) |
7 | 3, 6 | mpbir 234 | . . 3 ⊢ ∃𝑦 𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} |
8 | 7 | issetri 3413 | . 2 ⊢ {𝑤 ∣ 𝑤 ⊆ 𝑥} ∈ V |
9 | 1, 8 | eqeltri 2829 | 1 ⊢ 𝒫 𝑥 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∀wal 1540 = wceq 1542 ∃wex 1786 ∈ wcel 2113 {cab 2716 Vcvv 3397 ⊆ wss 3841 𝒫 cpw 4485 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 ax-sep 5164 ax-pow 5229 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3399 df-in 3848 df-ss 3858 df-pw 4487 |
This theorem is referenced by: pwexg 5242 pwnex 7494 inf3lem7 9163 dfac8 9628 dfac13 9635 ackbij1lem8 9720 dominf 9938 numthcor 9987 dominfac 10066 intwun 10228 wunex2 10231 eltsk2g 10244 inttsk 10267 tskcard 10274 intgru 10307 gruina 10311 axgroth6 10321 ismre 16957 fnmre 16958 mreacs 17025 isacs5lem 17888 pmtrfval 18689 istopon 21656 dmtopon 21667 tgdom 21722 isfbas 22573 bj-snglex 34775 exrecfnpw 35164 pwinfi 40700 ntrrn 41262 ntrf 41263 dssmapntrcls 41268 |
Copyright terms: Public domain | W3C validator |