Metamath Proof Explorer


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 φ x ψ
Assertion xpinintabd φ A × B x | ψ = w 𝒫 A × B | x w = A × B x ψ

Proof

Step Hyp Ref Expression
1 xpinintabd.x φ x ψ
2 1 inintabd φ A × B x | ψ = w 𝒫 A × B | x w = A × B x ψ