Theorem xpeq1i 5169

Description: Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.)

Hypothesis

Ref	Expression
xpeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
xpeq1i	⊢ (𝐴 × 𝐶) = (𝐵 × 𝐶)

Proof of Theorem xpeq1i

Step	Hyp	Ref	Expression
1		xpeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		xpeq1 5157	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 × 𝐶) = (𝐵 × 𝐶)

Syntax hints:   = wceq 1523   × cxp 5141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-opab 4746  df-xp 5149

This theorem is referenced by:  iunxpconst  5209  xpindi  5288  difxp2  5595  resdmres  5663  curry2  7317  mapsnconst  7945  mapsncnv  7946  cda1dif  9036  cdaassen  9042  infcda1  9053  geomulcvg  14651  hofcl  16946  evlsval  19567  matvsca2  20282  ovoliunnul  23321  vitalilem5  23426  lgam1  24835  finxp2o  33366  finxp3o  33367  poimirlem3  33542  poimirlem5  33544  poimirlem10  33549  poimirlem22  33561  poimirlem23  33562  mendvscafval  38077  binomcxplemnn0  38865  xpprsng  42435