![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > pwid | Structured version Unicode version |
Description: A set is a member of its power class. Theorem 87 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
pwid.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pwid |
![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwid.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | pwidg 3976 |
. 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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-v 3074 df-in 3438 df-ss 3445 df-pw 3965 |
This theorem is referenced by: r1ordg 8091 rankr1id 8175 cfss 8540 0ram 14194 evl1fval1lem 17884 bastg 18698 fincmp 19123 restlly 19214 ptbasfi 19281 zfbas 19596 ustfilxp 19914 metustfbasOLD 20267 metustfbas 20268 minveclem3b 21042 wilthlem3 22536 coinflipprob 27001 pwtrrVD 31874 mapdunirnN 35614 |
Copyright terms: Public domain | W3C validator |