Theorem elpwi2

Description: Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021) (Proof shortened by Wolf Lammen, 26-May-2024)

	Ref	Expression
Hypotheses	elpwi2.1	⊢ 𝐵 ∈ 𝑉
	elpwi2.2	⊢ 𝐴 ⊆ 𝐵
Assertion	elpwi2	⊢ 𝐴 ∈ 𝒫 𝐵

Proof

Step	Hyp	Ref	Expression
1		elpwi2.1	⊢ 𝐵 ∈ 𝑉
2		elpwi2.2	⊢ 𝐴 ⊆ 𝐵
3	1	elexi	⊢ 𝐵 ∈ V
4	3	elpw2	⊢ ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 )
5	2 4	mpbir	⊢ 𝐴 ∈ 𝒫 𝐵