Theorem inpw

Description: Two ways of expressing a collection of subsets as seen in df-ntr , unimax , and others. (Contributed by Zhi Wang, 27-Sep-2024)

	Ref	Expression
Assertion	inpw	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∩ 𝒫 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		dfin5	⊢ ( 𝐴 ∩ 𝒫 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝒫 𝐵 }
2		elpw2g	⊢ ( 𝐵 ∈ 𝑉 → ( 𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵 ) )
3	2	rabbidv	⊢ ( 𝐵 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝒫 𝐵 } = { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝐵 } )
4	1 3	eqtrid	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∩ 𝒫 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝐵 } )