Theorem xpeq2i 5285

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

Syntax hints:   = wceq 1624   × cxp 5256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-opab 4857  df-xp 5264

This theorem is referenced by:  xpindir  5404  xpssres  5584  difxp1  5709  xpima  5726  xpexgALT  7318  curry1  7429  fparlem3  7439  fparlem4  7440  xp1en  8203  xp2cda  9186  xpcdaen  9189  pwcda1  9200  pwcdandom  9673  yonedalem3b  17112  yonedalem3  17113  pws1  18808  pwsmgp  18810  xkoinjcn  21684  imasdsf1olem  22371  df0op2  28912  ho01i  28988  nmop0h  29151  mbfmcst  30622  0rrv  30814  cvmlift2lem12  31595  zrdivrng  34057