Theorem xpeq2i 5681

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

Syntax hints:   = wceq 1540   × cxp 5652

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-xp 5660

This theorem is referenced by:  xpindir  5814  xpssres  6005  difxp1  6154  xpima  6171  xpexgALT  7980  curry1  8103  fparlem3  8113  fparlem4  8114  xp1en  9071  djuunxp  9935  dju1dif  10187  djuassen  10193  xpdjuen  10194  infdju1  10204  yonedalem3b  18291  yonedalem3  18292  pws1  20285  pwsmgp  20287  xkoinjcn  23625  imasdsf1olem  24312  df0op2  31733  ho01i  31809  nmop0h  31972  mbfmcst  34291  0rrv  34483  cvmlift2lem12  35336  zrdivrng  37977  funcsetc1o  49382