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 4552 | . 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ 𝒫 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2108 Vcvv 3422 𝒫 cpw 4530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1542 df-ex 1784 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2817 df-v 3424 df-in 3890 df-ss 3900 df-pw 4532 |
This theorem is referenced by: pwnex 7587 r1ordg 9467 rankr1id 9551 cfss 9952 0ram 16649 evl1fval1lem 21406 bastg 22024 fincmp 22452 restlly 22542 ptbasfi 22640 zfbas 22955 ustfilxp 23272 minveclem3b 24497 wilthlem3 26124 coinflipprob 32346 mapdunirnN 39591 pwtrrVD 42334 vsetrec 46294 |
Copyright terms: Public domain | W3C validator |