Description: A set is a member of its power class. Theorem 87 of Suppes p. 47. (Contributed by NM, 5-Aug-1993)
Ref | Expression | ||
---|---|---|---|
Hypothesis | pwid.1 | ⊢ 𝐴 ∈ V | |
Assertion | pwid | ⊢ 𝐴 ∈ 𝒫 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwid.1 | ⊢ 𝐴 ∈ V | |
2 | pwidg | ⊢ ( 𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴 ) | |
3 | 1 2 | ax-mp | ⊢ 𝐴 ∈ 𝒫 𝐴 |