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 4544 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∈ wcel 2114 Vcvv 3496 ⊆ wss 3938 𝒫 cpw 4541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-in 3945 df-ss 3954 df-pw 4543 |
This theorem is referenced by: velpw 4546 0elpw 5258 snelpwi 5339 snelpw 5340 prelpw 5341 sspwb 5344 pwssun 5458 xpsspw 5684 knatar 7112 iunpw 7495 ssenen 8693 fissuni 8831 fipreima 8832 fipwuni 8892 dffi3 8897 marypha1lem 8899 inf3lem6 9098 tz9.12lem3 9220 rankonidlem 9259 r0weon 9440 infpwfien 9490 dfac5lem4 9554 dfac2b 9558 dfac12lem2 9572 enfin2i 9745 isfin1-3 9810 itunitc1 9844 hsmexlem4 9853 hsmexlem5 9854 axdc4lem 9879 pwfseqlem1 10082 eltsk2g 10175 ixxssxr 12753 ioof 12838 fzof 13038 hashbclem 13813 incexclem 15193 ramub1lem1 16364 ramub1lem2 16365 prdsplusg 16733 prdsmulr 16734 prdsvsca 16735 submrc 16901 isacs2 16926 isssc 17092 homaf 17292 catcfuccl 17371 catcxpccl 17459 clatl 17728 isacs4lem 17780 isacs5lem 17781 dprd2dlem1 19165 ablfac1b 19194 cssval 20828 tgdom 21588 distop 21605 fctop 21614 cctop 21616 ppttop 21617 pptbas 21618 epttop 21619 mretopd 21702 resttopon 21771 dishaus 21992 discmp 22008 cmpsublem 22009 cmpsub 22010 conncompid 22041 2ndcsep 22069 cldllycmp 22105 dislly 22107 iskgen3 22159 kgencn2 22167 txuni2 22175 dfac14 22228 prdstopn 22238 txcmplem1 22251 txcmplem2 22252 hmphdis 22406 fbssfi 22447 trfbas2 22453 uffixsn 22535 hauspwpwf1 22597 alexsubALTlem2 22658 ustuqtop0 22851 met1stc 23133 restmetu 23182 icccmplem1 23432 icccmplem2 23433 opnmbllem 24204 sqff1o 25761 incistruhgr 26866 upgrbi 26880 umgrbi 26888 upgr1e 26900 umgredg 26925 uspgr1e 27028 uhgrspansubgrlem 27074 eupth2lems 28019 sspval 28502 foresf1o 30267 cmpcref 31116 esumpcvgval 31339 esumcvg 31347 esum2d 31354 pwsiga 31391 difelsiga 31394 sigainb 31397 inelpisys 31415 pwldsys 31418 rossros 31441 measssd 31476 cntnevol 31489 ddemeas 31497 mbfmcnt 31528 br2base 31529 sxbrsigalem0 31531 oms0 31557 probun 31679 coinfliprv 31742 ballotth 31797 cvmcov2 32524 satfvel 32661 elfuns 33378 altxpsspw 33440 elhf2 33638 neibastop1 33709 neibastop2lem 33710 ctbssinf 34689 opnmbllem0 34930 heiborlem1 35091 heiborlem8 35098 pclfinN 37038 mapd1o 38786 elrfi 39298 ismrcd2 39303 istopclsd 39304 mrefg2 39311 isnacs3 39314 dfac11 39669 islssfg2 39678 lnr2i 39723 clsk1independent 40403 isotone2 40406 gneispace 40491 trsspwALT 41159 trsspwALT2 41160 trsspwALT3 41161 pwtrVD 41165 icof 41489 stoweidlem57 42349 intsal 42620 salexct 42624 sge0resplit 42695 sge0reuz 42736 omeiunltfirp 42808 smfpimbor1lem1 43080 sprvalpw 43649 sprsymrelf 43664 sprsymrelf1 43665 prprvalpw 43684 uspgropssxp 44026 uspgrsprf 44028 |
Copyright terms: Public domain | W3C validator |