Theorem sselpwd

Description: Membership in a power set. (Contributed by Thierry Arnoux, 18-May-2020)

	Ref	Expression
Hypotheses	sselpwd.1	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	sselpwd.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion	sselpwd	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sselpwd.1	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2		sselpwd.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
3	1 2	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
4	3 2	elpwd	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝐵 )