Theorem xpeq2i 5685

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

This proof depends on syntax axioms:   = wceq 1570   × cxp 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5174  df-xp 5664

This theorem is used by:  xpindir  5821  xpres  6024  difxp1  6174  xpima  6192  xpsnprg  7175  xpsntpg  7176  xpexgALT  8027  curry1  8152  fparlem3  8162  fparlem4  8163  xp1en  9120  djuunxp  10039  dju1dif  10290  djuassen  10296  xpdjuen  10297  infdju1  10307  yonedalem3b  18503  yonedalem3  18504  pws1  20605  pwsmgp  20607  xkoinjcn  24061  imasdsf1olem  24747  df0op2  32411  ho01i  32487  nmop0h  32650  cvmlift2lem12  36287  zrdivrng  39153  funcsetc1o  50963