Theorem xpeq2i 5658

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 5652	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 × 𝐴) = (𝐶 × 𝐵)

Syntax hints:   = wceq 1540   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5165  df-xp 5637

This theorem is referenced by:  xpindir  5788  xpssres  5978  difxp1  6126  xpima  6143  xpexgALT  7939  curry1  8060  fparlem3  8070  fparlem4  8071  xp1en  9004  djuunxp  9850  dju1dif  10102  djuassen  10108  xpdjuen  10109  infdju1  10119  yonedalem3b  18216  yonedalem3  18217  pws1  20210  pwsmgp  20212  xkoinjcn  23550  imasdsf1olem  24237  df0op2  31654  ho01i  31730  nmop0h  31893  mbfmcst  34223  0rrv  34415  cvmlift2lem12  35274  zrdivrng  37920  funcsetc1o  49459