![]() |
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 4980 | . 2 ⊢ (𝐴 ∈ V → 𝒫 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝒫 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2145 Vcvv 3351 𝒫 cpw 4297 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-ext 2751 ax-sep 4915 ax-pow 4974 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-v 3353 df-in 3730 df-ss 3737 df-pw 4299 |
This theorem is referenced by: p0ex 4984 pp0ex 4986 ord3ex 4987 abexssex 7296 fnpm 8017 canth2 8269 dffi3 8493 r1sucg 8796 r1pwALT 8873 rankuni 8890 rankc2 8898 rankxpu 8903 rankmapu 8905 rankxplim 8906 r0weon 9035 aceq3lem 9143 dfac5lem4 9149 dfac2a 9152 dfac2b 9153 dfac2OLD 9155 ackbij2lem2 9264 ackbij2lem3 9265 fin23lem17 9362 domtriomlem 9466 axdc2lem 9472 axdc3lem 9474 axdclem2 9544 alephsucpw 9594 canthp1lem1 9676 gchac 9705 gruina 9842 npex 10010 axcnex 10170 pnfxr 10294 mnfxr 10298 ixxex 12391 prdsval 16323 prdsds 16332 prdshom 16335 ismre 16458 fnmre 16459 fnmrc 16475 mrcfval 16476 mrisval 16498 wunfunc 16766 catcfuccl 16966 catcxpccl 17055 lubfval 17186 glbfval 17199 issubm 17555 issubg 17802 cntzfval 17960 sylow1lem2 18221 lsmfval 18260 pj1fval 18314 issubrg 18990 lssset 19144 lspfval 19186 islbs 19289 lbsext 19378 lbsexg 19379 sraval 19391 aspval 19543 ocvfval 20227 cssval 20243 isobs 20281 islinds 20365 istopon 20937 dmtopon 20948 fncld 21047 leordtval2 21237 cnpfval 21259 iscnp2 21264 kgenf 21565 xkoopn 21613 xkouni 21623 dfac14 21642 xkoccn 21643 prdstopn 21652 xkoco1cn 21681 xkoco2cn 21682 xkococn 21684 xkoinjcn 21711 isfbas 21853 uzrest 21921 acufl 21941 alexsubALTlem2 22072 tsmsval2 22153 ustfn 22225 ustn0 22244 ishtpy 22991 vitali 23601 sspval 27918 shex 28409 hsupval 28533 fpwrelmap 29848 fpwrelmapffs 29849 isrnsigaOLD 30515 dmvlsiga 30532 eulerpartlem1 30769 eulerpartgbij 30774 eulerpartlemmf 30777 coinflippv 30885 ballotlemoex 30887 reprval 31028 kur14lem9 31534 mpstval 31770 mclsrcl 31796 mclsval 31798 heibor1lem 33940 heibor 33952 idlval 34144 psubspset 35552 paddfval 35605 pclfvalN 35697 polfvalN 35712 psubclsetN 35744 docafvalN 36932 djafvalN 36944 dicval 36986 dochfval 37160 djhfval 37207 islpolN 37293 mzpclval 37814 eldiophb 37846 rpnnen3 38125 dfac11 38158 rgspnval 38264 clsk1independent 38870 dmvolsal 41081 ovnval 41275 smfresal 41515 sprbisymrel 42277 uspgrex 42286 uspgrbisymrelALT 42291 issubmgm 42317 lincop 42725 setrec2fun 42967 vsetrec 42977 elpglem3 42987 |
Copyright terms: Public domain | W3C validator |