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	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
Assertion	xpinintabd	⊢ ( 𝜑 → ( ( 𝐴 × 𝐵 ) ∩ ∩ { 𝑥 ∣ 𝜓 } ) = ∩ { 𝑤 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ ∃ 𝑥 ( 𝑤 = ( ( 𝐴 × 𝐵 ) ∩ 𝑥 ) ∧ 𝜓 ) } )

Proof

Step	Hyp	Ref	Expression
1		xpinintabd.x	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
2	1	inintabd	⊢ ( 𝜑 → ( ( 𝐴 × 𝐵 ) ∩ ∩ { 𝑥 ∣ 𝜓 } ) = ∩ { 𝑤 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∣ ∃ 𝑥 ( 𝑤 = ( ( 𝐴 × 𝐵 ) ∩ 𝑥 ) ∧ 𝜓 ) } )