Theorem xpeq2i 5704

Description: Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.)

Hypothesis

Ref	Expression
xpeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
xpeq2i	⊢ (𝐶 × 𝐴) = (𝐶 × 𝐵)

Proof of Theorem xpeq2i

Step	Hyp	Ref	Expression
1		xpeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		xpeq2 5698	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 × 𝐴) = (𝐶 × 𝐵)

Syntax hints:   = wceq 1542   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5212  df-xp 5683

This theorem is referenced by:  xpindir  5835  xpssres  6019  difxp1  6165  xpima  6182  xpexgALT  7968  curry1  8090  fparlem3  8100  fparlem4  8101  xp1en  9057  djuunxp  9916  dju1dif  10167  djuassen  10173  xpdjuen  10174  infdju1  10184  yonedalem3b  18232  yonedalem3  18233  pws1  20138  pwsmgp  20140  xkoinjcn  23191  imasdsf1olem  23879  df0op2  31005  ho01i  31081  nmop0h  31244  mbfmcst  33258  0rrv  33450  cvmlift2lem12  34305  zrdivrng  36821