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.) |
Ref | Expression |
---|---|
elpw.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
elpw | ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpw.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | sseq1 3589 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
3 | df-pw 4110 | . 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵} | |
4 | 1, 2, 3 | elab2 3323 | 1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∈ wcel 1977 Vcvv 3173 ⊆ wss 3540 𝒫 cpw 4108 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 df-ss 3554 df-pw 4110 |
This theorem is referenced by: selpw 4115 0elpw 4760 snelpwi 4839 snelpw 4840 prelpw 4841 sspwb 4844 pwssun 4944 xpsspw 5156 knatar 6507 iunpw 6870 ssenen 8019 fissuni 8154 fipreima 8155 fiin 8211 fipwuni 8215 dffi3 8220 marypha1lem 8222 inf3lem6 8413 tz9.12lem3 8535 rankonidlem 8574 r0weon 8718 infpwfien 8768 dfac5lem4 8832 dfac2 8836 dfac12lem2 8849 enfin2i 9026 isfin1-3 9091 itunitc1 9125 hsmexlem4 9134 hsmexlem5 9135 axdc4lem 9160 pwfseqlem1 9359 eltsk2g 9452 ixxssxr 12058 ioof 12142 fzof 12336 hashbclem 13093 incexclem 14407 ramub1lem1 15568 ramub1lem2 15569 prdsplusg 15941 prdsmulr 15942 prdsvsca 15943 submrc 16111 isacs2 16137 isssc 16303 homaf 16503 catcfuccl 16582 catcxpccl 16670 clatl 16939 fpwipodrs 16987 isacs4lem 16991 isacs5lem 16992 dprd2dlem1 18263 ablfac1b 18292 cssval 19845 tgdom 20593 distop 20610 fctop 20618 cctop 20620 ppttop 20621 pptbas 20622 epttop 20623 mretopd 20706 resttopon 20775 dishaus 20996 discmp 21011 cmpsublem 21012 cmpsub 21013 concompid 21044 2ndcsep 21072 cldllycmp 21108 dislly 21110 iskgen3 21162 kgencn2 21170 txuni2 21178 dfac14 21231 prdstopn 21241 txcmplem1 21254 txcmplem2 21255 hmphdis 21409 fbssfi 21451 trfbas2 21457 uffixsn 21539 hauspwpwf1 21601 alexsubALTlem2 21662 ustuqtop0 21854 met1stc 22136 restmetu 22185 icccmplem1 22433 icccmplem2 22434 opnmbllem 23175 sqff1o 24708 incistruhgr 25746 upgrbi 25760 umgrbi 25767 upgr1e 25779 umgredg 25812 umgra1 25855 uslgra1 25901 usgraedgrnv 25906 usgrarnedg 25913 usgraedg4 25916 usgrares1 25939 cusgrarn 25988 eupath2 26507 sspval 26962 foresf1o 28727 cmpcref 29245 esumpcvgval 29467 esumcvg 29475 esum2d 29482 pwsiga 29520 difelsiga 29523 sigainb 29526 inelpisys 29544 pwldsys 29547 rossros 29570 measssd 29605 cntnevol 29618 ddemeas 29626 mbfmcnt 29657 br2base 29658 sxbrsigalem0 29660 oms0 29686 probun 29808 coinfliprv 29871 ballotth 29926 cvmcov2 30511 elfuns 31192 altxpsspw 31254 elhf2 31452 neibastop1 31524 neibastop2lem 31525 opnmbllem0 32615 heiborlem1 32780 heiborlem8 32787 pclfinN 34204 mapd1o 35955 elrfi 36275 ismrcd2 36280 istopclsd 36281 mrefg2 36288 isnacs3 36291 dfac11 36650 islssfg2 36659 lnr2i 36705 clsk1independent 37364 isotone1 37366 isotone2 37367 gneispace 37452 trsspwALT 38067 trsspwALT2 38068 trsspwALT3 38069 pwtrVD 38081 icof 38406 stoweidlem57 38950 intsal 39224 salexct 39228 sge0resplit 39299 sge0reuz 39340 omeiunltfirp 39409 smfpimbor1lem1 39683 uspgr1e 40470 uhgrspansubgrlem 40514 eupth2lems 41406 |
Copyright terms: Public domain | W3C validator |