| 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 2108 Vcvv 3480 𝒫 cpw 4600 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-pow 5365 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: p0ex 5384 pp0ex 5386 ord3ex 5387 abexssex 7995 mptmpoopabbrd 8105 fnpm 8874 canth2 9170 dffi3 9471 r1sucg 9809 r1pwALT 9886 rankuni 9903 rankc2 9911 rankxpu 9916 rankmapu 9918 rankxplim 9919 r0weon 10052 aceq3lem 10160 dfac5lem4 10166 dfac5lem4OLD 10168 dfac2a 10170 dfac2b 10171 pwdju1 10231 ackbij2lem2 10279 ackbij2lem3 10280 fin23lem17 10378 domtriomlem 10482 axdc2lem 10488 axdc3lem 10490 axdclem2 10560 alephsucpw 10610 canthp1lem1 10692 gchac 10721 gruina 10858 npex 11026 nrex1 11104 pnfex 11314 mnfxr 11318 ixxex 13398 prdsvallem 17499 prdsds 17509 prdshom 17512 ismre 17633 fnmre 17634 fnmrc 17650 mrcfval 17651 mrisval 17673 wunfunc 17946 catcfuccl 18163 catcxpccl 18252 lubfval 18395 glbfval 18408 issubmgm 18715 issubm 18816 issubg 19144 cntzfval 19338 sylow1lem2 19617 lsmfval 19656 pj1fval 19712 issubrng 20547 issubrg 20571 rgspnval 20612 lssset 20931 lspfval 20971 islbs 21075 lbsext 21165 lbsexg 21166 sraval 21174 ocvfval 21684 cssval 21700 isobs 21740 islinds 21829 aspval 21893 istopon 22918 dmtopon 22929 fncld 23030 leordtval2 23220 cnpfval 23242 iscnp2 23247 kgenf 23549 xkoopn 23597 xkouni 23607 dfac14 23626 xkoccn 23627 prdstopn 23636 xkoco1cn 23665 xkoco2cn 23666 xkococn 23668 xkoinjcn 23695 isfbas 23837 uzrest 23905 acufl 23925 alexsubALTlem2 24056 tsmsval2 24138 ustfn 24210 ustn0 24229 ishtpy 25004 vitali 25648 madefi 27950 sspval 30742 shex 31231 hsupval 31353 fpwrelmap 32744 fpwrelmapffs 32745 dmvlsiga 34130 eulerpartlem1 34369 eulerpartgbij 34374 eulerpartlemmf 34377 coinflippv 34486 ballotlemoex 34488 reprval 34625 kur14lem9 35219 satfvsuclem1 35364 mpstval 35540 mclsrcl 35566 mclsval 35568 heibor1lem 37816 heibor 37828 idlval 38020 psubspset 39746 paddfval 39799 pclfvalN 39891 polfvalN 39906 psubclsetN 39938 docafvalN 41124 djafvalN 41136 dicval 41178 dochfval 41352 djhfval 41399 islpolN 41485 mzpclval 42736 eldiophb 42768 rpnnen3 43044 dfac11 43074 clsk1independent 44059 dmvolsal 46361 ovnval 46556 smfresal 46803 sprbisymrel 47486 grtri 47907 uspgrex 48066 uspgrbisymrelALT 48071 lincop 48325 setrec2fun 49211 elpglem3 49232 |
| Copyright terms: Public domain | W3C validator |