# Metamath Proof Explorer

## 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}\in \mathrm{V}$
xpmapen.2 ${⊢}{B}\in \mathrm{V}$
xpmapen.3 ${⊢}{C}\in \mathrm{V}$
Assertion xpmapen ${⊢}\left({\left({A}×{B}\right)}^{{C}}\right)\approx \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)$

### Proof

Step Hyp Ref Expression
1 xpmapen.1 ${⊢}{A}\in \mathrm{V}$
2 xpmapen.2 ${⊢}{B}\in \mathrm{V}$
3 xpmapen.3 ${⊢}{C}\in \mathrm{V}$
4 2fveq3 ${⊢}{w}={z}\to {1}^{st}\left({x}\left({w}\right)\right)={1}^{st}\left({x}\left({z}\right)\right)$
5 4 cbvmptv ${⊢}\left({w}\in {C}⟼{1}^{st}\left({x}\left({w}\right)\right)\right)=\left({z}\in {C}⟼{1}^{st}\left({x}\left({z}\right)\right)\right)$
6 2fveq3 ${⊢}{w}={z}\to {2}^{nd}\left({x}\left({w}\right)\right)={2}^{nd}\left({x}\left({z}\right)\right)$
7 6 cbvmptv ${⊢}\left({w}\in {C}⟼{2}^{nd}\left({x}\left({w}\right)\right)\right)=\left({z}\in {C}⟼{2}^{nd}\left({x}\left({z}\right)\right)\right)$
8 fveq2 ${⊢}{w}={z}\to {1}^{st}\left({y}\right)\left({w}\right)={1}^{st}\left({y}\right)\left({z}\right)$
9 fveq2 ${⊢}{w}={z}\to {2}^{nd}\left({y}\right)\left({w}\right)={2}^{nd}\left({y}\right)\left({z}\right)$
10 8 9 opeq12d ${⊢}{w}={z}\to ⟨{1}^{st}\left({y}\right)\left({w}\right),{2}^{nd}\left({y}\right)\left({w}\right)⟩=⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩$
11 10 cbvmptv ${⊢}\left({w}\in {C}⟼⟨{1}^{st}\left({y}\right)\left({w}\right),{2}^{nd}\left({y}\right)\left({w}\right)⟩\right)=\left({z}\in {C}⟼⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩\right)$
12 1 2 3 5 7 11 xpmapenlem ${⊢}\left({\left({A}×{B}\right)}^{{C}}\right)\approx \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)$