![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elpw2g | Structured version Visualization version Unicode version |
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.) |
Ref | Expression |
---|---|
elpw2g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpwi 3960 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ssexg 4549 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | elpwg 3959 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | biimparc 490 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | syldan 473 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | expcom 437 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 6 | impbid2 208 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-v 3047 df-in 3411 df-ss 3418 df-pw 3953 |
This theorem is referenced by: elpw2 4567 pwnss 4568 knatar 6248 pw2f1olem 7676 fineqvlem 7786 elfir 7929 marypha1 7948 r1sscl 8256 tskwe 8384 dfac8alem 8460 acni2 8477 fin1ai 8723 fin2i 8725 fin23lem7 8746 fin23lem11 8747 isfin2-2 8749 fin23lem39 8780 isf34lem1 8802 isf34lem2 8803 isf34lem4 8807 isf34lem5 8808 fin1a2lem7 8836 fin1a2lem12 8841 canthnumlem 9073 canthp1lem2 9078 wunss 9137 tsken 9179 tskss 9183 gruss 9221 ramub1lem1 14984 ismre 15496 mreintcl 15501 mremre 15510 submre 15511 mrcval 15516 mrccl 15517 mrcun 15528 ismri 15537 mreexd 15548 mreexexlem4d 15553 acsfiel 15560 isacs1i 15563 catcoppccl 16003 acsdrsel 16413 acsdrscl 16416 acsficl 16417 pmtrval 17092 pmtrrn 17098 opsrval 18698 istopg 19925 uniopn 19927 iscld 20042 ntrval 20051 clsval 20052 discld 20105 mretopd 20108 neival 20118 isnei 20119 lpval 20155 restdis 20194 ordtbaslem 20204 ordtuni 20206 cncls 20290 cndis 20307 tgcmp 20416 hauscmplem 20421 comppfsc 20547 elkgen 20551 xkoopn 20604 elqtop 20712 kqffn 20740 isfbas 20844 filss 20868 snfbas 20881 elfg 20886 fbasrn 20899 ufilss 20920 fixufil 20937 cfinufil 20943 ufinffr 20944 ufilen 20945 fin1aufil 20947 rnelfmlem 20967 flimclslem 20999 hauspwpwf1 21002 supnfcls 21035 flimfnfcls 21043 ptcmplem1 21067 tsmsfbas 21142 blfvalps 21398 blfps 21421 blf 21422 bcthlem5 22296 minveclem3b 22370 minveclem3bOLD 22382 sigaclcuni 28940 sigaclcu2 28942 pwsiga 28952 erdsze2lem2 29927 cvmsval 29989 cvmsss2 29997 neibastop2lem 31016 tailf 31031 fin2so 31932 sdclem1 32072 elrfirn 35537 elrfirn2 35538 istopclsd 35542 nacsfix 35554 dnnumch1 35902 |
Copyright terms: Public domain | W3C validator |