Theorem xpeq2i 5136

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

Syntax hints:   = wceq 1483   × cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-opab 4713  df-xp 5120

This theorem is referenced by:  xpindir  5256  xpssres  5434  difxp1  5559  xpima  5576  xpexgALT  7161  curry1  7269  fparlem3  7279  fparlem4  7280  xp1en  8046  xp2cda  9002  xpcdaen  9005  pwcda1  9016  pwcdandom  9489  yonedalem3b  16919  yonedalem3  16920  pws1  18616  pwsmgp  18618  xkoinjcn  21490  imasdsf1olem  22178  df0op2  28611  ho01i  28687  nmop0h  28850  mbfmcst  30321  0rrv  30513  cvmlift2lem12  31296  zrdivrng  33752