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	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶 ) → 𝐴 ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		elpwi	⊢ ( 𝐵 ∈ 𝒫 𝐶 → 𝐵 ⊆ 𝐶 )
2	1	sseld	⊢ ( 𝐵 ∈ 𝒫 𝐶 → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐶 ) )
3	2	impcom	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶 ) → 𝐴 ∈ 𝐶 )