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	|- ( ph -> E. x ps )
Assertion	xpinintabd	|- ( ph -> ( ( A X. B ) i^i |^| { x | ps } ) = |^| { w e. ~P ( A X. B ) | E. x ( w = ( ( A X. B ) i^i x ) /\ ps ) } )

Proof

Step	Hyp	Ref	Expression
1		xpinintabd.x	|- ( ph -> E. x ps )
2	1	inintabd	|- ( ph -> ( ( A X. B ) i^i |^| { x | ps } ) = |^| { w e. ~P ( A X. B ) | E. x ( w = ( ( A X. B ) i^i x ) /\ ps ) } )