![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > selpw | Structured version Visualization version Unicode version |
Description: Setvar variable membership in a power class (common case). See elpw 3969. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
selpw |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3060 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | elpw 3969 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-v 3059 df-in 3423 df-ss 3430 df-pw 3965 |
This theorem is referenced by: elpwg 3971 pwss 3978 snsspw 4156 pwpr 4208 pwtp 4209 pwv 4211 sspwuni 4381 iinpw 4384 iunpwss 4385 pwuni 4645 ssextss 4668 pwin 4757 pwunss 4758 sorpsscmpl 6609 iunpw 6632 ordpwsuc 6669 fabexg 6776 abexssex 6802 qsss 7450 mapval2 7527 pmsspw 7532 uniixp 7571 fineqvlem 7812 fival 7952 hartogslem1 8083 tskwe 8410 cfval2 8716 cflim3 8718 cflim2 8719 cfslb 8722 compsscnvlem 8826 fin1a2lem13 8868 axdc3lem 8906 fpwwe2lem1 9082 fpwwe2lem11 9091 fpwwe2lem12 9092 fpwwe 9097 canthwe 9102 axgroth5 9275 axgroth6 9279 wuncn 9620 ishashinf 12659 vdwmc 14977 ramub2 15020 ram0 15029 restsspw 15379 ismred 15557 mremre 15559 mreacs 15613 acsfn 15614 submacs 16661 subgacs 16901 nsgacs 16902 sylow2alem2 17319 sylow2a 17320 sylow3lem3 17330 sylow3lem6 17333 dprdres 17710 subgdmdprd 17716 pgpfac1lem5 17761 subrgmre 18081 subsubrg2 18084 lssintcl 18236 lssmre 18238 lssacs 18239 cssmre 19305 istopon 19989 isbasis2g 20012 tgval2 20020 unitg 20031 distop 20060 cldss2 20094 ntreq0 20142 discld 20154 toponmre 20158 neisspw 20172 restdis 20243 cnntr 20340 isnrm2 20423 cmpcovf 20455 fincmp 20457 cmpsublem 20463 cmpsub 20464 cmpcld 20466 cmpfi 20472 is1stc2 20506 2ndcdisj 20520 llyi 20538 nllyi 20539 nlly2i 20540 llynlly 20541 subislly 20545 restnlly 20546 llyrest 20549 llyidm 20552 nllyidm 20553 islocfin 20581 ptuni2 20640 prdstopn 20692 qtoptop2 20763 qtopuni 20766 tgqtop 20776 isfbas2 20899 isfild 20922 elfg 20935 cfinfil 20957 csdfil 20958 supfil 20959 isufil2 20972 filssufilg 20975 uffix 20985 ufildr 20995 fin1aufil 20996 alexsubb 21110 alexsubALTlem1 21111 alexsubALT 21115 ptcmplem5 21120 cldsubg 21174 ustfn 21265 ustfilxp 21276 ustn0 21284 dscopn 21637 voliunlem2 22553 vitali 22620 shex 26914 dfch2 27109 fpwrelmap 28367 xrsclat 28491 cmpcref 28726 sigaex 28980 sigaval 28981 insiga 29008 sigapisys 29026 sigaldsys 29030 measdivcst 29096 ballotlem2 29370 erdszelem7 29969 erdsze2lem2 29976 rellyscon 30023 dffr5 30442 neibastop2lem 31065 neibastop3 31067 topmeet 31069 topjoin 31070 neifg 31076 bj-snglss 31609 dissneqlem 31787 topdifinfeq 31798 heibor1lem 32186 psubspset 33354 psubclsetN 33546 lcdlss 35232 ismrcd1 35585 pw2f1ocnv 35937 filnm 35993 hbtlem6 36033 sdrgacs 36112 elmapintrab 36227 clcnvlem 36275 psshepw 36429 nbuhgr 39461 nbuhgr2vtx1edgblem 39469 submgmacs 40077 |
Copyright terms: Public domain | W3C validator |