![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elpw2 | Structured version Visualization version GIF version |
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |
Ref | Expression |
---|---|
elpw2.1 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
elpw2 | ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpw2.1 | . 2 ⊢ 𝐵 ∈ V | |
2 | elpw2g 5340 | . 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∈ wcel 2099 Vcvv 3469 ⊆ wss 3944 𝒫 cpw 4598 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 ax-sep 5293 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-rab 3428 df-v 3471 df-in 3951 df-ss 3961 df-pw 4600 |
This theorem is referenced by: elpwi2 5342 axpweq 5344 knatar 7359 dffi3 9440 marypha1lem 9442 r1pwss 9793 rankr1bg 9812 pwwf 9816 unwf 9819 rankval2 9827 uniwf 9828 rankpwi 9832 dfac2a 10138 dfac12lem2 10153 axdc4lem 10464 axdclem 10528 incexclem 15800 rpnnen2lem1 16176 rpnnen2lem2 16177 sadfval 16412 smufval 16437 smupf 16438 vdwapf 16926 prdshom 17434 mreacs 17623 acsfn 17624 lubeldm 18330 lubval 18333 glbeldm 18343 glbval 18346 clatlem 18479 clatlubcl2 18481 clatglbcl2 18483 issubmgm 18647 issubm 18740 issubg 19065 cntzval 19256 sylow1lem2 19538 lsmvalx 19578 pj1fval 19633 issubrng 20466 issubrg 20492 islss 20800 lspval 20841 lspcl 20842 islbs 20943 lbsextlem1 21028 lbsextlem3 21030 lbsextlem4 21031 sraval 21042 ocvval 21579 isobs 21634 islinds 21723 aspval 21786 uncmp 23281 cmpfi 23286 cmpfii 23287 2ndc1stc 23329 1stcrest 23331 hausllycmp 23372 lly1stc 23374 1stckgenlem 23431 txlly 23514 txnlly 23515 tx1stc 23528 basqtop 23589 tgqtop 23590 alexsubALTlem3 23927 alexsubALTlem4 23928 alexsubALT 23929 cncfval 24782 cnllycmp 24856 ovolficcss 25372 ovolval 25376 ovolicc2 25425 ismbl 25429 mblsplit 25435 voliunlem3 25455 vitalilem4 25514 vitalilem5 25515 dvfval 25800 dvnfval 25826 cpnfval 25836 plyval 26101 dmarea 26863 wilthlem2 26975 issh 30992 ocval 31064 spanval 31117 hsupval 31118 sshjval 31134 sshjval3 31138 zarcls 33398 zartopn 33399 sigagensiga 33683 dya2iocuni 33826 coinflippv 34026 ballotlemelo 34030 ballotth 34080 erdszelem1 34724 kur14lem9 34747 kur14 34749 cnllysconn 34778 elmpst 35069 mclsrcl 35094 mclsval 35096 icoreresf 36754 cntotbnd 37191 heibor1lem 37204 heibor 37216 isidl 37409 igenval 37456 paddval 39195 pclvalN 39287 polvalN 39302 docavalN 40520 djavalN 40532 dicval 40573 dochval 40748 djhval 40795 lpolconN 40884 elpwbi 41627 elmzpcl 42058 eldiophb 42089 rpnnen3 42365 islssfgi 42408 hbt 42466 elmnc 42472 itgoval 42497 itgocn 42500 rgspnval 42504 elpglem2 48056 |
Copyright terms: Public domain | W3C validator |