Theorem xpeq2i 5689

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

Syntax hints:   = wceq 1567   × cxp 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5178  df-xp 5668

This theorem is referenced by:  xpindir  5821  xpssres  6018  difxp1  6163  xpima  6181  xpexgALT  7977  curry1  8098  fparlem3  8108  fparlem4  8109  xp1en  9050  djuunxp  9906  dju1dif  10155  djuassen  10161  xpdjuen  10162  infdju1  10172  yonedalem3b  18334  yonedalem3  18335  pws1  20405  pwsmgp  20407  xkoinjcn  23812  imasdsf1olem  24498  df0op2  32044  ho01i  32120  nmop0h  32283  mbfmcst  34593  0rrv  34785  cvmlift2lem12  35704  zrdivrng  38491  funcsetc1o  50159