Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Replacement
Theorems requiring subset and intersection existence
pwnss
Next ⟩
pwne
Metamath Proof Explorer
Ascii
Unicode
Theorem
pwnss
Description:
The power set of a set is never a subset.
(Contributed by
Stefan O'Rear
, 22-Feb-2015)
Ref
Expression
Assertion
pwnss
⊢
A
∈
V
→
¬
𝒫
A
⊆
A
Proof
Step
Hyp
Ref
Expression
1
rru
⊢
¬
x
∈
A
|
¬
x
∈
x
∈
A
2
ssel
⊢
𝒫
A
⊆
A
→
x
∈
A
|
¬
x
∈
x
∈
𝒫
A
→
x
∈
A
|
¬
x
∈
x
∈
A
3
1
2
mtoi
⊢
𝒫
A
⊆
A
→
¬
x
∈
A
|
¬
x
∈
x
∈
𝒫
A
4
ssrab2
⊢
x
∈
A
|
¬
x
∈
x
⊆
A
5
elpw2g
⊢
A
∈
V
→
x
∈
A
|
¬
x
∈
x
∈
𝒫
A
↔
x
∈
A
|
¬
x
∈
x
⊆
A
6
4
5
mpbiri
⊢
A
∈
V
→
x
∈
A
|
¬
x
∈
x
∈
𝒫
A
7
3
6
nsyl3
⊢
A
∈
V
→
¬
𝒫
A
⊆
A