![]() |
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 5378 | . 2 ⊢ (𝐴 ∈ V → 𝒫 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝒫 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 Vcvv 3461 𝒫 cpw 4604 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-pow 5365 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-ss 3961 df-pw 4606 |
This theorem is referenced by: p0ex 5384 pp0ex 5386 ord3ex 5387 abexssex 7975 mptmpoopabbrd 8085 fnpm 8853 canth2 9155 dffi3 9456 r1sucg 9794 r1pwALT 9871 rankuni 9888 rankc2 9896 rankxpu 9901 rankmapu 9903 rankxplim 9904 r0weon 10037 aceq3lem 10145 dfac5lem4 10151 dfac2a 10154 dfac2b 10155 pwdju1 10215 ackbij2lem2 10265 ackbij2lem3 10266 fin23lem17 10363 domtriomlem 10467 axdc2lem 10473 axdc3lem 10475 axdclem2 10545 alephsucpw 10595 canthp1lem1 10677 gchac 10706 gruina 10843 npex 11011 nrex1 11089 pnfex 11299 mnfxr 11303 ixxex 13370 prdsvallem 17439 prdsds 17449 prdshom 17452 ismre 17573 fnmre 17574 fnmrc 17590 mrcfval 17591 mrisval 17613 wunfunc 17890 wunfuncOLD 17891 catcfuccl 18111 catcfucclOLD 18112 catcxpccl 18201 catcxpcclOLD 18202 lubfval 18345 glbfval 18358 issubmgm 18665 issubm 18763 issubg 19089 cntzfval 19283 sylow1lem2 19566 lsmfval 19605 pj1fval 19661 issubrng 20496 issubrg 20522 lssset 20829 lspfval 20869 islbs 20973 lbsext 21063 lbsexg 21064 sraval 21072 ocvfval 21615 cssval 21631 isobs 21671 islinds 21760 aspval 21823 istopon 22858 dmtopon 22869 fncld 22970 leordtval2 23160 cnpfval 23182 iscnp2 23187 kgenf 23489 xkoopn 23537 xkouni 23547 dfac14 23566 xkoccn 23567 prdstopn 23576 xkoco1cn 23605 xkoco2cn 23606 xkococn 23608 xkoinjcn 23635 isfbas 23777 uzrest 23845 acufl 23865 alexsubALTlem2 23996 tsmsval2 24078 ustfn 24150 ustn0 24169 ishtpy 24942 vitali 25586 sspval 30605 shex 31094 hsupval 31216 fpwrelmap 32597 fpwrelmapffs 32598 dmvlsiga 33879 eulerpartlem1 34118 eulerpartgbij 34123 eulerpartlemmf 34126 coinflippv 34234 ballotlemoex 34236 reprval 34373 kur14lem9 34955 satfvsuclem1 35100 mpstval 35276 mclsrcl 35302 mclsval 35304 heibor1lem 37413 heibor 37425 idlval 37617 psubspset 39347 paddfval 39400 pclfvalN 39492 polfvalN 39507 psubclsetN 39539 docafvalN 40725 djafvalN 40737 dicval 40779 dochfval 40953 djhfval 41000 islpolN 41086 mzpclval 42287 eldiophb 42319 rpnnen3 42595 dfac11 42628 rgspnval 42734 clsk1independent 43618 dmvolsal 45872 ovnval 46067 smfresal 46314 sprbisymrel 46976 uspgrex 47398 uspgrbisymrelALT 47403 lincop 47662 setrec2fun 48309 elpglem3 48330 |
Copyright terms: Public domain | W3C validator |