![]() |
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 4364 | . 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ 𝒫 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 Vcvv 3385 𝒫 cpw 4349 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-v 3387 df-in 3776 df-ss 3783 df-pw 4351 |
This theorem is referenced by: pwnex 7201 r1ordg 8891 rankr1id 8975 cfss 9375 0ram 16057 evl1fval1lem 20016 bastg 21099 fincmp 21525 restlly 21615 ptbasfi 21713 zfbas 22028 ustfilxp 22344 minveclem3b 23538 wilthlem3 25148 coinflipprob 31058 mapdunirnN 37671 pwtrrVD 39821 vsetrec 43248 |
Copyright terms: Public domain | W3C validator |