Metamath Proof Explorer
Description: A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)
|
|
Ref |
Expression |
|
Assertion |
pwidg |
|
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
elex |
|
| 2 |
|
ssidd |
|
| 3 |
1 2
|
elpwd |
|