Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elpw | Structured version Visualization version GIF version |
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.) (Proof shortened by BJ, 31-Dec-2023.) |
Ref | Expression |
---|---|
elpw.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
elpw | ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpw.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | elpwg 4513 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∈ wcel 2110 Vcvv 3405 ⊆ wss 3863 𝒫 cpw 4510 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3407 df-in 3870 df-ss 3880 df-pw 4512 |
This theorem is referenced by: velpw 4515 0elpw 5244 snelpwi 5326 snelpw 5327 prelpw 5328 sspwb 5331 pwssun 5448 xpsspw 5676 knatar 7163 iunpw 7553 ssenen 8817 fissuni 8978 fipreima 8979 fipwuni 9039 dffi3 9044 marypha1lem 9046 inf3lem6 9245 tz9.12lem3 9402 rankonidlem 9441 r0weon 9623 infpwfien 9673 dfac5lem4 9737 dfac2b 9741 dfac12lem2 9755 enfin2i 9932 isfin1-3 9997 itunitc1 10031 hsmexlem4 10040 hsmexlem5 10041 axdc4lem 10066 pwfseqlem1 10269 eltsk2g 10362 ixxssxr 12944 ioof 13032 fzof 13237 hashbclem 14013 incexclem 15397 ramub1lem1 16576 ramub1lem2 16577 prdsplusg 16960 prdsmulr 16961 prdsvsca 16962 submrc 17128 isacs2 17153 isssc 17322 homaf 17533 catcfuccl 17622 catcfucclOLD 17623 catcxpccl 17711 catcxpcclOLD 17712 clatl 18011 isacs4lem 18047 isacs5lem 18048 dprd2dlem1 19425 ablfac1b 19454 cssval 20641 tgdom 21872 distop 21889 fctop 21898 cctop 21900 ppttop 21901 pptbas 21902 epttop 21903 mretopd 21986 resttopon 22055 dishaus 22276 discmp 22292 cmpsublem 22293 cmpsub 22294 conncompid 22325 2ndcsep 22353 cldllycmp 22389 dislly 22391 iskgen3 22443 kgencn2 22451 txuni2 22459 dfac14 22512 prdstopn 22522 txcmplem1 22535 txcmplem2 22536 hmphdis 22690 fbssfi 22731 trfbas2 22737 uffixsn 22819 hauspwpwf1 22881 alexsubALTlem2 22942 ustuqtop0 23135 met1stc 23416 restmetu 23465 icccmplem1 23716 icccmplem2 23717 opnmbllem 24495 sqff1o 26061 incistruhgr 27167 upgrbi 27181 umgrbi 27189 upgr1e 27201 umgredg 27226 uspgr1e 27329 uhgrspansubgrlem 27375 eupth2lems 28318 sspval 28801 foresf1o 30566 cmpcref 31511 esumpcvgval 31755 esumcvg 31763 esum2d 31770 pwsiga 31807 difelsiga 31810 sigainb 31813 pwldsys 31834 rossros 31857 measssd 31892 cntnevol 31905 ddemeas 31913 mbfmcnt 31944 br2base 31945 sxbrsigalem0 31947 oms0 31973 probun 32095 coinfliprv 32158 ballotth 32213 cvmcov2 32947 satfvel 33084 0slt1s 33757 oldf 33775 newf 33776 leftf 33783 rightf 33784 elfuns 33951 altxpsspw 34013 elhf2 34211 neibastop1 34282 neibastop2lem 34283 ctbssinf 35311 opnmbllem0 35548 heiborlem1 35704 heiborlem8 35711 pclfinN 37649 mapd1o 39397 elrfi 40217 ismrcd2 40222 istopclsd 40223 mrefg2 40230 isnacs3 40233 dfac11 40588 islssfg2 40597 lnr2i 40642 clsk1independent 41331 isotone2 41334 gneispace 41419 ismnushort 41590 trsspwALT 42109 trsspwALT2 42110 trsspwALT3 42111 pwtrVD 42115 icof 42430 stoweidlem57 43271 intsal 43542 salexct 43546 sge0resplit 43617 sge0reuz 43658 omeiunltfirp 43730 smfpimbor1lem1 44002 sprvalpw 44603 sprsymrelf 44618 sprsymrelf1 44619 prprvalpw 44638 uspgropssxp 44977 uspgrsprf 44979 |
Copyright terms: Public domain | W3C validator |