Theorem elpwd

Description: Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020)

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

Proof

Step	Hyp	Ref	Expression
1		elpwd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		elpwd.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
3		elpwg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )
4	1 3	syl	⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )
5	2 4	mpbird	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝐵 )