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	$$⊢\left(A\in V\wedge B\in W\right)\to A\times B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		iunid	$$⊢\bigcup _{y\in B}\left\{y\right\}=B$$
2	1	xpeq2i	$$⊢A\times \bigcup _{y\in B}\left\{y\right\}=A\times B$$
3		xpiundi	$$⊢A\times \bigcup _{y\in B}\left\{y\right\}=\bigcup _{y\in B}\left(A\times \left\{y\right\}\right)$$
4	2 3	eqtr3i	$$⊢A\times B=\bigcup _{y\in B}\left(A\times \left\{y\right\}\right)$$
5		id	$$⊢B\in W\to B\in W$$
6		fconstmpt	$$⊢A\times \left\{y\right\}=\left(x\in A⟼y\right)$$
7		mptexg	$$⊢A\in V\to \left(x\in A⟼y\right)\in \mathrm{V}$$
8	6 7	eqeltrid	$$⊢A\in V\to A\times \left\{y\right\}\in \mathrm{V}$$
9	8	ralrimivw	$$⊢A\in V\to \forall y\in BA\times \left\{y\right\}\in \mathrm{V}$$
10		iunexg	$$⊢\left(B\in W\wedge \forall y\in BA\times \left\{y\right\}\in \mathrm{V}\right)\to \bigcup _{y\in B}\left(A\times \left\{y\right\}\right)\in \mathrm{V}$$
11	5 9 10	syl2anr	$$⊢\left(A\in V\wedge B\in W\right)\to \bigcup _{y\in B}\left(A\times \left\{y\right\}\right)\in \mathrm{V}$$
12	4 11	eqeltrid	$$⊢\left(A\in V\wedge B\in W\right)\to A\times B\in \mathrm{V}$$