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	$$⊢B\in V\to A\cap 𝒫B=\left\{x\in A|x\subseteq B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfin5	$$⊢A\cap 𝒫B=\left\{x\in A|x\in 𝒫B\right\}$$
2		elpw2g	$$⊢B\in V\to \left(x\in 𝒫B\leftrightarrow x\subseteq B\right)$$
3	2	rabbidv	$$⊢B\in V\to \left\{x\in A|x\in 𝒫B\right\}=\left\{x\in A|x\subseteq B\right\}$$
4	1 3	eqtrid	$$⊢B\in V\to A\cap 𝒫B=\left\{x\in A|x\subseteq B\right\}$$