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 5271 | . 2 ⊢ (𝐴 ∈ V → 𝒫 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝒫 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 Vcvv 3495 𝒫 cpw 4537 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-pow 5258 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-v 3497 df-in 3942 df-ss 3951 df-pw 4539 |
This theorem is referenced by: p0ex 5276 pp0ex 5278 ord3ex 5279 abexssex 7662 fnpm 8404 canth2 8659 dffi3 8884 r1sucg 9187 r1pwALT 9264 rankuni 9281 rankc2 9289 rankxpu 9294 rankmapu 9296 rankxplim 9297 r0weon 9427 aceq3lem 9535 dfac5lem4 9541 dfac2a 9544 dfac2b 9545 pwdju1 9605 ackbij2lem2 9651 ackbij2lem3 9652 fin23lem17 9749 domtriomlem 9853 axdc2lem 9859 axdc3lem 9861 axdclem2 9931 alephsucpw 9981 canthp1lem1 10063 gchac 10092 gruina 10229 npex 10397 nrex1 10475 pnfex 10683 mnfxr 10687 ixxex 12739 prdsval 16718 prdsds 16727 prdshom 16730 ismre 16851 fnmre 16852 fnmrc 16868 mrcfval 16869 mrisval 16891 wunfunc 17159 catcfuccl 17359 catcxpccl 17447 lubfval 17578 glbfval 17591 issubm 17958 issubg 18219 cntzfval 18390 sylow1lem2 18655 lsmfval 18694 pj1fval 18751 issubrg 19466 lssset 19636 lspfval 19676 islbs 19779 lbsext 19866 lbsexg 19867 sraval 19879 aspval 20032 ocvfval 20740 cssval 20756 isobs 20794 islinds 20883 istopon 21450 dmtopon 21461 fncld 21560 leordtval2 21750 cnpfval 21772 iscnp2 21777 kgenf 22079 xkoopn 22127 xkouni 22137 dfac14 22156 xkoccn 22157 prdstopn 22166 xkoco1cn 22195 xkoco2cn 22196 xkococn 22198 xkoinjcn 22225 isfbas 22367 uzrest 22435 acufl 22455 alexsubALTlem2 22586 tsmsval2 22667 ustfn 22739 ustn0 22758 ishtpy 23505 vitali 24143 sspval 28428 shex 28917 hsupval 29039 fpwrelmap 30396 fpwrelmapffs 30397 dmvlsiga 31288 eulerpartlem1 31525 eulerpartgbij 31530 eulerpartlemmf 31533 coinflippv 31641 ballotlemoex 31643 reprval 31781 kur14lem9 32359 satfvsuclem1 32504 mpstval 32680 mclsrcl 32706 mclsval 32708 heibor1lem 34970 heibor 34982 idlval 35174 psubspset 36762 paddfval 36815 pclfvalN 36907 polfvalN 36922 psubclsetN 36954 docafvalN 38140 djafvalN 38152 dicval 38194 dochfval 38368 djhfval 38415 islpolN 38501 mzpclval 39202 eldiophb 39234 rpnnen3 39509 dfac11 39542 rgspnval 39648 clsk1independent 40276 dmvolsal 42510 ovnval 42704 smfresal 42944 sprbisymrel 43508 uspgrex 43872 uspgrbisymrelALT 43877 issubmgm 43903 lincop 44361 setrec2fun 44693 vsetrec 44703 elpglem3 44713 |
Copyright terms: Public domain | W3C validator |