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 4543 | . 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 |
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-in 3942 df-ss 3951 df-pw 4539 |
This theorem is referenced by: velpw 4545 0elpw 5248 snelpwi 5328 snelpw 5329 prelpw 5330 sspwb 5333 pwssun 5449 xpsspw 5676 knatar 7099 iunpw 7481 ssenen 8680 fissuni 8818 fipreima 8819 fipwuni 8879 dffi3 8884 marypha1lem 8886 inf3lem6 9085 tz9.12lem3 9207 rankonidlem 9246 r0weon 9427 infpwfien 9477 dfac5lem4 9541 dfac2b 9545 dfac12lem2 9559 enfin2i 9732 isfin1-3 9797 itunitc1 9831 hsmexlem4 9840 hsmexlem5 9841 axdc4lem 9866 pwfseqlem1 10069 eltsk2g 10162 ixxssxr 12740 ioof 12825 fzof 13025 hashbclem 13800 incexclem 15181 ramub1lem1 16352 ramub1lem2 16353 prdsplusg 16721 prdsmulr 16722 prdsvsca 16723 submrc 16889 isacs2 16914 isssc 17080 homaf 17280 catcfuccl 17359 catcxpccl 17447 clatl 17716 isacs4lem 17768 isacs5lem 17769 dprd2dlem1 19094 ablfac1b 19123 cssval 20756 tgdom 21516 distop 21533 fctop 21542 cctop 21544 ppttop 21545 pptbas 21546 epttop 21547 mretopd 21630 resttopon 21699 dishaus 21920 discmp 21936 cmpsublem 21937 cmpsub 21938 conncompid 21969 2ndcsep 21997 cldllycmp 22033 dislly 22035 iskgen3 22087 kgencn2 22095 txuni2 22103 dfac14 22156 prdstopn 22166 txcmplem1 22179 txcmplem2 22180 hmphdis 22334 fbssfi 22375 trfbas2 22381 uffixsn 22463 hauspwpwf1 22525 alexsubALTlem2 22586 ustuqtop0 22778 met1stc 23060 restmetu 23109 icccmplem1 23359 icccmplem2 23360 opnmbllem 24131 sqff1o 25687 incistruhgr 26792 upgrbi 26806 umgrbi 26814 upgr1e 26826 umgredg 26851 uspgr1e 26954 uhgrspansubgrlem 27000 eupth2lems 27945 sspval 28428 foresf1o 30193 cmpcref 31014 esumpcvgval 31237 esumcvg 31245 esum2d 31252 pwsiga 31289 difelsiga 31292 sigainb 31295 inelpisys 31313 pwldsys 31316 rossros 31339 measssd 31374 cntnevol 31387 ddemeas 31395 mbfmcnt 31426 br2base 31427 sxbrsigalem0 31429 oms0 31455 probun 31577 coinfliprv 31640 ballotth 31695 cvmcov2 32420 satfvel 32557 elfuns 33274 altxpsspw 33336 elhf2 33534 neibastop1 33605 neibastop2lem 33606 ctbssinf 34570 opnmbllem0 34810 heiborlem1 34972 heiborlem8 34979 pclfinN 36918 mapd1o 38666 elrfi 39171 ismrcd2 39176 istopclsd 39177 mrefg2 39184 isnacs3 39187 dfac11 39542 islssfg2 39551 lnr2i 39596 clsk1independent 40276 isotone2 40279 gneispace 40364 trsspwALT 41032 trsspwALT2 41033 trsspwALT3 41034 pwtrVD 41038 icof 41362 stoweidlem57 42223 intsal 42494 salexct 42498 sge0resplit 42569 sge0reuz 42610 omeiunltfirp 42682 smfpimbor1lem1 42954 sprvalpw 43489 sprsymrelf 43504 sprsymrelf1 43505 prprvalpw 43524 uspgropssxp 43866 uspgrsprf 43868 |
Copyright terms: Public domain | W3C validator |