Theorem xpeq2i 5727

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

Syntax hints:   = wceq 1537   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-xp 5706

This theorem is referenced by:  xpindir  5859  xpssres  6047  difxp1  6196  xpima  6213  xpexgALT  8022  curry1  8145  fparlem3  8155  fparlem4  8156  xp1en  9123  djuunxp  9990  dju1dif  10242  djuassen  10248  xpdjuen  10249  infdju1  10259  yonedalem3b  18349  yonedalem3  18350  pws1  20348  pwsmgp  20350  xkoinjcn  23716  imasdsf1olem  24404  df0op2  31784  ho01i  31860  nmop0h  32023  mbfmcst  34224  0rrv  34416  cvmlift2lem12  35282  zrdivrng  37913