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 )