Theorem bj-sselpwuni

Description: Quantitative version of ssexg : a subset of an element of a class is an element of the powerclass of the union of that class. (Contributed by BJ, 6-Apr-2024)

	Ref	Expression
Assertion	bj-sselpwuni	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝒫 ∪ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		ssexg	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ V )
2		ssuni	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ⊆ ∪ 𝑉 )
3	1 2	elpwd	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝒫 ∪ 𝑉 )