Theorem xpinintabd

Description: Value of the intersection of Cartesian product with the intersection of a nonempty class. (Contributed by RP, 12-Aug-2020)

	Ref	Expression
Hypothesis	xpinintabd.x	$$⊢\phi \to \exists x\psi$$
Assertion	xpinintabd	$$⊢\phi \to \left(A\times B\right)\cap \bigcap \left\{x|\psi \right\}=\bigcap \left\{w\in 𝒫\left(A\times B\right)|\exists x\left(w=\left(A\times B\right)\cap x\wedge \psi \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		xpinintabd.x	$$⊢\phi \to \exists x\psi$$
2	1	inintabd	$$⊢\phi \to \left(A\times B\right)\cap \bigcap \left\{x|\psi \right\}=\bigcap \left\{w\in 𝒫\left(A\times B\right)|\exists x\left(w=\left(A\times B\right)\cap x\wedge \psi \right)\right\}$$