Metamath Proof Explorer

Theorem iunxpconst

Description: Membership in a union of Cartesian products when the second factor is constant. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Assertion iunxpconst 
|- U_ x e. A ( { x } X. B ) = ( A X. B )

Proof

Step Hyp Ref Expression
1 xpiundir 
 |-  ( U_ x e. A { x } X. B ) = U_ x e. A ( { x } X. B )
2 iunid 
 |-  U_ x e. A { x } = A
3 2 xpeq1i 
 |-  ( U_ x e. A { x } X. B ) = ( A X. B )
4 1 3 eqtr3i 
 |-  U_ x e. A ( { x } X. B ) = ( A X. B )