Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Power classes
elelpwi
Next ⟩
sspw
Metamath Proof Explorer
Ascii
Unicode
Theorem
elelpwi
Description:
If
A
belongs to a part of
C
, then
A
belongs to
C
.
(Contributed by
FL
, 3-Aug-2009)
Ref
Expression
Assertion
elelpwi
⊢
A
∈
B
∧
B
∈
𝒫
C
→
A
∈
C
Proof
Step
Hyp
Ref
Expression
1
elpwi
⊢
B
∈
𝒫
C
→
B
⊆
C
2
1
sseld
⊢
B
∈
𝒫
C
→
A
∈
B
→
A
∈
C
3
2
impcom
⊢
A
∈
B
∧
B
∈
𝒫
C
→
A
∈
C