![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elpw2 | Structured version Visualization version Unicode version |
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |
Ref | Expression |
---|---|
elpw2.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
elpw2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpw2.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | elpw2g 4579 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-v 3058 df-in 3422 df-ss 3429 df-pw 3964 |
This theorem is referenced by: axpweq 4593 knatar 6272 canth 6273 dffi3 7970 marypha1lem 7972 r1pwss 8280 rankr1bg 8299 pwwf 8303 unwf 8306 rankval2 8314 uniwf 8315 rankpwi 8319 aceq3lem 8576 dfac2a 8585 dfac12lem2 8599 axdc3lem4 8908 axdc4lem 8910 axdclem 8974 grothpw 9276 uzf 11190 ixxf 11673 fzf 11816 incexclem 13942 rpnnen2lem1 14315 rpnnen2lem2 14316 bitsf 14448 sadfval 14474 smufval 14499 smupf 14500 vdwapf 14970 prdsval 15401 prdsds 15410 prdshom 15413 mreacs 15612 acsfn 15613 wunnat 15909 lubeldm 16275 lubval 16278 glbeldm 16288 glbval 16291 clatlem 16405 clatlubcl2 16407 clatglbcl2 16409 issubm 16642 issubg 16865 cntzval 17023 sylow1lem2 17299 lsmvalx 17339 pj1fval 17392 issubrg 18056 islss 18206 lspval 18246 lspcl 18247 islbs 18347 lbsextlem1 18429 lbsextlem3 18431 lbsextlem4 18432 sraval 18447 aspval 18600 ocvfval 19277 ocvval 19278 isobs 19331 islinds 19415 leordtval2 20276 cnpfval 20298 iscnp2 20303 uncmp 20466 cmpfi 20471 cmpfii 20472 2ndc1stc 20514 1stcrest 20516 islly2 20547 hausllycmp 20557 lly1stc 20559 1stckgenlem 20616 xkotf 20648 txlly 20699 txnlly 20700 tx1stc 20713 basqtop 20774 tgqtop 20775 alexsubALTlem3 21112 alexsubALTlem4 21113 alexsubALT 21114 sszcld 21883 cncfval 21968 cnllycmp 22032 bndth 22034 ishtpy 22051 ovolficcss 22470 ovolval 22474 ovolvalOLD 22475 ovolicc2 22524 ismbl 22528 mblsplit 22534 voliunlem3 22553 vitalilem4 22617 vitalilem5 22618 dvfval 22900 dvnfval 22924 cpnfval 22934 plyval 23195 dmarea 23931 wilthlem2 24042 umgrabi 25759 issh 26909 ocval 26981 spanval 27034 hsupval 27035 sshjval 27051 sshjval3 27055 fpwrelmap 28366 sigagensiga 29011 dya2iocuni 29153 coinflippv 29364 ballotlemelo 29368 ballotlem2 29369 ballotth 29418 ballotthOLD 29456 erdszelem1 29962 kur14lem9 29985 kur14 29987 cnllyscon 30016 elmpst 30222 mclsrcl 30247 mclsval 30249 icoreresf 31799 cover2 32084 cntotbnd 32172 heibor1lem 32185 heibor 32197 isidl 32291 igenval 32338 paddval 33407 pclvalN 33499 polvalN 33514 docavalN 34735 djavalN 34747 dicval 34788 dochval 34963 djhval 35010 lpolconN 35099 elmzpcl 35612 eldiophb 35643 rpnnen3 35931 islssfgi 35974 hbt 36033 elmnc 36039 itgoval 36071 itgocn 36074 rgspnval 36078 issubmgm 40061 |
Copyright terms: Public domain | W3C validator |