| 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 5333 | . 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∈ wcel 2108 Vcvv 3480 ⊆ wss 3951 𝒫 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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-in 3958 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: elpwi2 5335 axpweq 5351 knatar 7377 dffi3 9471 marypha1lem 9473 r1pwss 9824 rankr1bg 9843 pwwf 9847 unwf 9850 rankval2 9858 uniwf 9859 rankpwi 9863 dfac2a 10170 dfac12lem2 10185 axdc4lem 10495 axdclem 10559 incexclem 15872 rpnnen2lem1 16250 rpnnen2lem2 16251 sadfval 16489 smufval 16514 smupf 16515 vdwapf 17010 prdshom 17512 mreacs 17701 acsfn 17702 lubeldm 18398 lubval 18401 glbeldm 18411 glbval 18414 clatlem 18547 clatlubcl2 18549 clatglbcl2 18551 issubmgm 18715 issubm 18816 issubg 19144 cntzval 19339 sylow1lem2 19617 lsmvalx 19657 pj1fval 19712 issubrng 20547 issubrg 20571 rgspnval 20612 islss 20932 lspval 20973 lspcl 20974 islbs 21075 lbsextlem1 21160 lbsextlem3 21162 lbsextlem4 21163 sraval 21174 ocvval 21685 isobs 21740 islinds 21829 aspval 21893 uncmp 23411 cmpfi 23416 cmpfii 23417 2ndc1stc 23459 1stcrest 23461 hausllycmp 23502 lly1stc 23504 1stckgenlem 23561 txlly 23644 txnlly 23645 tx1stc 23658 basqtop 23719 tgqtop 23720 alexsubALTlem3 24057 alexsubALTlem4 24058 alexsubALT 24059 cncfval 24914 cnllycmp 24988 ovolficcss 25504 ovolval 25508 ovolicc2 25557 ismbl 25561 mblsplit 25567 voliunlem3 25587 vitalilem4 25646 vitalilem5 25647 dvfval 25932 dvnfval 25958 cpnfval 25968 plyval 26232 dmarea 27000 wilthlem2 27112 issh 31227 ocval 31299 spanval 31352 hsupval 31353 sshjval 31369 sshjval3 31373 zarcls 33873 zartopn 33874 sigagensiga 34142 dya2iocuni 34285 coinflippv 34486 ballotlemelo 34490 ballotth 34540 erdszelem1 35196 kur14lem9 35219 kur14 35221 cnllysconn 35250 elmpst 35541 mclsrcl 35566 mclsval 35568 icoreresf 37353 cntotbnd 37803 heibor1lem 37816 heibor 37828 isidl 38021 igenval 38068 paddval 39800 pclvalN 39892 polvalN 39907 docavalN 41125 djavalN 41137 dicval 41178 dochval 41353 djhval 41400 lpolconN 41489 elpwbi 42269 elmzpcl 42737 eldiophb 42768 rpnnen3 43044 islssfgi 43084 hbt 43142 elmnc 43148 itgoval 43173 itgocn 43176 elpglem2 49231 |
| Copyright terms: Public domain | W3C validator |