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  18220  yonedalem3  18221  pws1  20245  pwsmgp  20247  xkoinjcn  23607  imasdsf1olem  24294  df0op2  31731  ho01i  31807  nmop0h  31970  mbfmcst  34243  0rrv  34435  cvmlift2lem12  35294  zrdivrng  37940  funcsetc1o  49479