![]() |
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. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
pwex.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
pwex | ⊢ 𝒫 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | pwexg 5092 | . 2 ⊢ (𝐴 ∈ V → 𝒫 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝒫 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3398 𝒫 cpw 4379 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 ax-sep 5019 ax-pow 5079 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-v 3400 df-in 3799 df-ss 3806 df-pw 4381 |
This theorem is referenced by: p0ex 5097 pp0ex 5099 ord3ex 5100 abexssex 7429 fnpm 8150 canth2 8403 dffi3 8627 r1sucg 8931 r1pwALT 9008 rankuni 9025 rankc2 9033 rankxpu 9038 rankmapu 9040 rankxplim 9041 r0weon 9170 aceq3lem 9278 dfac5lem4 9284 dfac2a 9287 dfac2b 9288 dfac2OLD 9290 ackbij2lem2 9399 ackbij2lem3 9400 fin23lem17 9497 domtriomlem 9601 axdc2lem 9607 axdc3lem 9609 axdclem2 9679 alephsucpw 9729 canthp1lem1 9811 gchac 9840 gruina 9977 npex 10145 nrex1 10223 pnfex 10431 mnfxr 10436 ixxex 12502 prdsval 16505 prdsds 16514 prdshom 16517 ismre 16640 fnmre 16641 fnmrc 16657 mrcfval 16658 mrisval 16680 wunfunc 16948 catcfuccl 17148 catcxpccl 17237 lubfval 17368 glbfval 17381 issubm 17737 issubg 17982 cntzfval 18140 sylow1lem2 18402 lsmfval 18441 pj1fval 18495 issubrg 19176 lssset 19330 lspfval 19372 islbs 19475 lbsext 19564 lbsexg 19565 sraval 19577 aspval 19729 ocvfval 20413 cssval 20429 isobs 20467 islinds 20556 istopon 21128 dmtopon 21139 fncld 21238 leordtval2 21428 cnpfval 21450 iscnp2 21455 kgenf 21757 xkoopn 21805 xkouni 21815 dfac14 21834 xkoccn 21835 prdstopn 21844 xkoco1cn 21873 xkoco2cn 21874 xkococn 21876 xkoinjcn 21903 isfbas 22045 uzrest 22113 acufl 22133 alexsubALTlem2 22264 tsmsval2 22345 ustfn 22417 ustn0 22436 ishtpy 23183 vitali 23821 sspval 28154 shex 28645 hsupval 28769 fpwrelmap 30078 fpwrelmapffs 30079 isrnsigaOLD 30777 dmvlsiga 30794 eulerpartlem1 31031 eulerpartgbij 31036 eulerpartlemmf 31039 coinflippv 31148 ballotlemoex 31150 reprval 31294 kur14lem9 31799 mpstval 32035 mclsrcl 32061 mclsval 32063 heibor1lem 34237 heibor 34249 idlval 34441 psubspset 35903 paddfval 35956 pclfvalN 36048 polfvalN 36063 psubclsetN 36095 docafvalN 37281 djafvalN 37293 dicval 37335 dochfval 37509 djhfval 37556 islpolN 37642 mzpclval 38258 eldiophb 38290 rpnnen3 38568 dfac11 38601 rgspnval 38707 clsk1independent 39310 dmvolsal 41498 ovnval 41692 smfresal 41932 sprbisymrel 42448 uspgrex 42783 uspgrbisymrelALT 42788 issubmgm 42814 lincop 43222 setrec2fun 43554 vsetrec 43564 elpglem3 43574 |
Copyright terms: Public domain | W3C validator |