![]() |
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 4624 | . 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ 𝒫 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 Vcvv 3477 𝒫 cpw 4604 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1539 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-ss 3979 df-pw 4606 |
This theorem is referenced by: pwnex 7777 r1ordg 9815 rankr1id 9899 cfss 10302 0ram 17053 evl1fval1lem 22349 bastg 22988 fincmp 23416 restlly 23506 ptbasfi 23604 zfbas 23919 ustfilxp 24236 minveclem3b 25475 wilthlem3 27127 coinflipprob 34460 mapdunirnN 41632 pwtrrVD 44822 vsetrec 48933 |
Copyright terms: Public domain | W3C validator |