![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pwex | Structured version Visualization version GIF version |
Description: Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Ref | Expression |
---|---|
zfpowcl.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
pwex | ⊢ 𝒫 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zfpowcl.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | pweq 4194 | . . 3 ⊢ (𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴) | |
3 | 2 | eleq1d 2715 | . 2 ⊢ (𝑧 = 𝐴 → (𝒫 𝑧 ∈ V ↔ 𝒫 𝐴 ∈ V)) |
4 | df-pw 4193 | . . 3 ⊢ 𝒫 𝑧 = {𝑦 ∣ 𝑦 ⊆ 𝑧} | |
5 | axpow2 4875 | . . . . . 6 ⊢ ∃𝑥∀𝑦(𝑦 ⊆ 𝑧 → 𝑦 ∈ 𝑥) | |
6 | 5 | bm1.3ii 4817 | . . . . 5 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧) |
7 | abeq2 2761 | . . . . . 6 ⊢ (𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧)) | |
8 | 7 | exbii 1814 | . . . . 5 ⊢ (∃𝑥 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧)) |
9 | 6, 8 | mpbir 221 | . . . 4 ⊢ ∃𝑥 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} |
10 | 9 | issetri 3241 | . . 3 ⊢ {𝑦 ∣ 𝑦 ⊆ 𝑧} ∈ V |
11 | 4, 10 | eqeltri 2726 | . 2 ⊢ 𝒫 𝑧 ∈ V |
12 | 1, 3, 11 | vtocl 3290 | 1 ⊢ 𝒫 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∀wal 1521 = wceq 1523 ∃wex 1744 ∈ wcel 2030 {cab 2637 Vcvv 3231 ⊆ wss 3607 𝒫 cpw 4191 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-pow 4873 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-v 3233 df-in 3614 df-ss 3621 df-pw 4193 |
This theorem is referenced by: vpwex 4879 p0ex 4883 pp0ex 4885 ord3ex 4886 abexssex 7191 fnpm 7907 canth2 8154 dffi3 8378 r1sucg 8670 r1pwALT 8747 rankuni 8764 rankc2 8772 rankxpu 8777 rankmapu 8779 rankxplim 8780 r0weon 8873 aceq3lem 8981 dfac5lem4 8987 dfac2a 8990 dfac2 8991 ackbij2lem2 9100 ackbij2lem3 9101 fin23lem17 9198 domtriomlem 9302 axdc2lem 9308 axdc3lem 9310 axdclem2 9380 alephsucpw 9430 canthp1lem1 9512 gchac 9541 gruina 9678 npex 9846 axcnex 10006 pnfxr 10130 mnfxr 10134 ixxex 12224 prdsval 16162 prdsds 16171 prdshom 16174 ismre 16297 fnmre 16298 fnmrc 16314 mrcfval 16315 mrisval 16337 wunfunc 16606 catcfuccl 16806 catcxpccl 16894 lubfval 17025 glbfval 17038 issubm 17394 issubg 17641 cntzfval 17799 sylow1lem2 18060 lsmfval 18099 pj1fval 18153 issubrg 18828 lssset 18982 lspfval 19021 islbs 19124 lbsext 19211 lbsexg 19212 sraval 19224 aspval 19376 ocvfval 20058 cssval 20074 isobs 20112 islinds 20196 istopon 20765 dmtopon 20775 fncld 20874 leordtval2 21064 cnpfval 21086 iscnp2 21091 kgenf 21392 xkoopn 21440 xkouni 21450 dfac14 21469 xkoccn 21470 prdstopn 21479 xkoco1cn 21508 xkoco2cn 21509 xkococn 21511 xkoinjcn 21538 isfbas 21680 uzrest 21748 acufl 21768 alexsubALTlem2 21899 tsmsval2 21980 ustfn 22052 ustn0 22071 ishtpy 22818 vitali 23427 sspval 27706 shex 28197 hsupval 28321 fpwrelmap 29636 fpwrelmapffs 29637 isrnsigaOLD 30303 dmvlsiga 30320 eulerpartlem1 30557 eulerpartgbij 30562 eulerpartlemmf 30565 coinflippv 30673 ballotlemoex 30675 reprval 30816 kur14lem9 31322 mpstval 31558 mclsrcl 31584 mclsval 31586 heibor1lem 33738 heibor 33750 idlval 33942 psubspset 35348 paddfval 35401 pclfvalN 35493 polfvalN 35508 psubclsetN 35540 docafvalN 36728 djafvalN 36740 dicval 36782 dochfval 36956 djhfval 37003 islpolN 37089 mzpclval 37605 eldiophb 37637 rpnnen3 37916 dfac11 37949 rgspnval 38055 clsk1independent 38661 dmvolsal 40882 ovnval 41076 smfresal 41316 sprbisymrel 42074 uspgrex 42083 uspgrbisymrelALT 42088 issubmgm 42114 lincop 42522 setrec2fun 42764 vsetrec 42774 elpglem3 42784 |
Copyright terms: Public domain | W3C validator |