Theorem xpmapen

Description: Equinumerosity law for set exponentiation of a Cartesian product. Exercise 4.47 of Mendelson p. 255. (Contributed by NM, 23-Feb-2004) (Proof shortened by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Hypotheses	xpmapen.1	|- A e. _V
	xpmapen.2	|- B e. _V
	xpmapen.3	|- C e. _V
Assertion	xpmapen	|- ( ( A X. B ) ^m C ) ~~ ( ( A ^m C ) X. ( B ^m C ) )

Proof

Step	Hyp	Ref	Expression
1		xpmapen.1	|- A e. _V
2		xpmapen.2	|- B e. _V
3		xpmapen.3	|- C e. _V
4		2fveq3	|- ( w = z -> ( 1st ` ( x ` w ) ) = ( 1st ` ( x ` z ) ) )
5	4	cbvmptv	|- ( w e. C |-> ( 1st ` ( x ` w ) ) ) = ( z e. C |-> ( 1st ` ( x ` z ) ) )
6		2fveq3	|- ( w = z -> ( 2nd ` ( x ` w ) ) = ( 2nd ` ( x ` z ) ) )
7	6	cbvmptv	|- ( w e. C |-> ( 2nd ` ( x ` w ) ) ) = ( z e. C |-> ( 2nd ` ( x ` z ) ) )
8		fveq2	|- ( w = z -> ( ( 1st ` y ) ` w ) = ( ( 1st ` y ) ` z ) )
9		fveq2	|- ( w = z -> ( ( 2nd ` y ) ` w ) = ( ( 2nd ` y ) ` z ) )
10	8 9	opeq12d	|- ( w = z -> <. ( ( 1st ` y ) ` w ) , ( ( 2nd ` y ) ` w ) >. = <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. )
11	10	cbvmptv	|- ( w e. C |-> <. ( ( 1st ` y ) ` w ) , ( ( 2nd ` y ) ` w ) >. ) = ( z e. C |-> <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. )
12	1 2 3 5 7 11	xpmapenlem	|- ( ( A X. B ) ^m C ) ~~ ( ( A ^m C ) X. ( B ^m C ) )