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 5239 | . 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∈ wcel 2105 Vcvv 3495 ⊆ wss 3935 𝒫 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 |
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-nfc 2963 df-rab 3147 df-v 3497 df-in 3942 df-ss 3951 df-pw 4539 |
This theorem is referenced by: axpweq 5257 knatar 7099 dffi3 8884 marypha1lem 8886 r1pwss 9202 rankr1bg 9221 pwwf 9225 unwf 9228 rankval2 9236 uniwf 9237 rankpwi 9241 dfac2a 9544 dfac12lem2 9559 axdc4lem 9866 axdclem 9930 incexclem 15181 rpnnen2lem1 15557 rpnnen2lem2 15558 sadfval 15791 smufval 15816 smupf 15817 vdwapf 16298 prdshom 16730 mreacs 16919 acsfn 16920 lubeldm 17581 lubval 17584 glbeldm 17594 glbval 17597 clatlem 17711 clatlubcl2 17713 clatglbcl2 17715 issubm 17958 issubg 18219 cntzval 18391 sylow1lem2 18655 lsmvalx 18695 pj1fval 18751 issubrg 19466 islss 19637 lspval 19678 lspcl 19679 islbs 19779 lbsextlem1 19861 lbsextlem3 19863 lbsextlem4 19864 sraval 19879 aspval 20032 ocvval 20741 isobs 20794 islinds 20883 uncmp 21941 cmpfi 21946 cmpfii 21947 2ndc1stc 21989 1stcrest 21991 hausllycmp 22032 lly1stc 22034 1stckgenlem 22091 txlly 22174 txnlly 22175 tx1stc 22188 basqtop 22249 tgqtop 22250 alexsubALTlem3 22587 alexsubALTlem4 22588 alexsubALT 22589 cncfval 23425 cnllycmp 23489 ovolficcss 23999 ovolval 24003 ovolicc2 24052 ismbl 24056 mblsplit 24062 voliunlem3 24082 vitalilem4 24141 vitalilem5 24142 dvfval 24424 dvnfval 24448 cpnfval 24458 plyval 24712 dmarea 25463 wilthlem2 25574 issh 28913 ocval 28985 spanval 29038 hsupval 29039 sshjval 29055 sshjval3 29059 sigagensiga 31300 dya2iocuni 31441 coinflippv 31641 ballotlemelo 31645 ballotth 31695 erdszelem1 32336 kur14lem9 32359 kur14 32361 cnllysconn 32390 elmpst 32681 mclsrcl 32706 mclsval 32708 icoreresf 34516 cntotbnd 34957 heibor1lem 34970 heibor 34982 isidl 35175 igenval 35222 paddval 36816 pclvalN 36908 polvalN 36923 docavalN 38141 djavalN 38153 dicval 38194 dochval 38369 djhval 38416 lpolconN 38505 elpwbi 38996 elmzpcl 39203 eldiophb 39234 rpnnen3 39509 islssfgi 39552 hbt 39610 elmnc 39616 itgoval 39641 itgocn 39644 rgspnval 39648 issubmgm 43903 elpglem2 44712 |
Copyright terms: Public domain | W3C validator |