This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpexgALT

Description: Alternate proof of xpexg requiring Replacement ( ax-rep ) but not Power Set ( ax-pow ). (Contributed by Mario Carneiro, 20-May-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion xpexgALT 
|- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )

Proof

Step Hyp Ref Expression
1 iunid 
 |-  U_ y e. B { y } = B
2 1 xpeq2i 
 |-  ( A X. U_ y e. B { y } ) = ( A X. B )
3 xpiundi 
 |-  ( A X. U_ y e. B { y } ) = U_ y e. B ( A X. { y } )
4 2 3 eqtr3i 
 |-  ( A X. B ) = U_ y e. B ( A X. { y } )
5 id 
 |-  ( B e. W -> B e. W )
6 fconstmpt 
 |-  ( A X. { y } ) = ( x e. A |-> y )
7 mptexg 
 |-  ( A e. V -> ( x e. A |-> y ) e. _V )
8 6 7 eqeltrid 
 |-  ( A e. V -> ( A X. { y } ) e. _V )
9 8 ralrimivw 
 |-  ( A e. V -> A. y e. B ( A X. { y } ) e. _V )
10 iunexg 
 |-  ( ( B e. W /\ A. y e. B ( A X. { y } ) e. _V ) -> U_ y e. B ( A X. { y } ) e. _V )
11 5 9 10 syl2anr 
 |-  ( ( A e. V /\ B e. W ) -> U_ y e. B ( A X. { y } ) e. _V )
12 4 11 eqeltrid 
 |-  ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )