![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pwid | Structured version Visualization version GIF 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 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
pwid | ⊢ 𝐴 ∈ 𝒫 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwid.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | pwidg 4617 | . 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ 𝒫 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 Vcvv 3462 𝒫 cpw 4597 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ss 3963 df-pw 4599 |
This theorem is referenced by: pwnex 7759 r1ordg 9814 rankr1id 9898 cfss 10299 0ram 17017 evl1fval1lem 22318 bastg 22957 fincmp 23385 restlly 23475 ptbasfi 23573 zfbas 23888 ustfilxp 24205 minveclem3b 25444 wilthlem3 27095 coinflipprob 34326 mapdunirnN 41362 pwtrrVD 44538 vsetrec 48485 |
Copyright terms: Public domain | W3C validator |