![]() |
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 3951 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ssexg 4542 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | elpwg 3950 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | biimparc 495 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | syldan 478 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | expcom 442 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 6 | impbid2 209 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 |
This theorem depends on definitions: df-bi 190 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-v 3033 df-in 3397 df-ss 3404 df-pw 3944 |
This theorem is referenced by: elpw2 4565 pwnss 4566 knatar 6266 pw2f1olem 7694 fineqvlem 7804 elfir 7947 marypha1 7966 r1sscl 8274 tskwe 8402 dfac8alem 8478 acni2 8495 fin1ai 8741 fin2i 8743 fin23lem7 8764 fin23lem11 8765 isfin2-2 8767 fin23lem39 8798 isf34lem1 8820 isf34lem2 8821 isf34lem4 8825 isf34lem5 8826 fin1a2lem7 8854 fin1a2lem12 8859 canthnumlem 9091 canthp1lem2 9096 wunss 9155 tsken 9197 tskss 9201 gruss 9239 ramub1lem1 15063 ismre 15574 mreintcl 15579 mremre 15588 submre 15589 mrcval 15594 mrccl 15595 mrcun 15606 ismri 15615 mreexd 15626 mreexexlem4d 15631 acsfiel 15638 isacs1i 15641 catcoppccl 16081 acsdrsel 16491 acsdrscl 16494 acsficl 16495 pmtrval 17170 pmtrrn 17176 opsrval 18775 istopg 20002 uniopn 20004 iscld 20119 ntrval 20128 clsval 20129 discld 20182 mretopd 20185 neival 20195 isnei 20196 lpval 20232 restdis 20271 ordtbaslem 20281 ordtuni 20283 cncls 20367 cndis 20384 tgcmp 20493 hauscmplem 20498 comppfsc 20624 elkgen 20628 xkoopn 20681 elqtop 20789 kqffn 20817 isfbas 20922 filss 20946 snfbas 20959 elfg 20964 fbasrn 20977 ufilss 20998 fixufil 21015 cfinufil 21021 ufinffr 21022 ufilen 21023 fin1aufil 21025 rnelfmlem 21045 flimclslem 21077 hauspwpwf1 21080 supnfcls 21113 flimfnfcls 21121 ptcmplem1 21145 tsmsfbas 21220 blfvalps 21476 blfps 21499 blf 21500 bcthlem5 22374 minveclem3b 22448 minveclem3bOLD 22460 sigaclcuni 29014 sigaclcu2 29016 pwsiga 29026 erdsze2lem2 29999 cvmsval 30061 cvmsss2 30069 neibastop2lem 31087 tailf 31102 fin2so 31996 sdclem1 32136 elrfirn 35608 elrfirn2 35609 istopclsd 35613 nacsfix 35625 dnnumch1 35973 elpwi2 37501 |
Copyright terms: Public domain | W3C validator |