Theorem xpeq1i 5338

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

Syntax hints:   = wceq 1653   × cxp 5310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-opab 4906  df-xp 5318

This theorem is referenced by:  iunxpconst  5378  xpindi  5459  difxp2  5777  resdmres  5844  curry2  7509  mapsnconst  8143  mapsncnv  8144  cda1dif  9286  cdaassen  9292  infcda1  9303  geomulcvg  14945  hofcl  17214  evlsval  19841  matvsca2  20559  ovoliunnul  23615  vitalilem5  23720  lgam1  25142  finxp2o  33734  finxp3o  33735  poimirlem3  33901  poimirlem5  33903  poimirlem10  33908  poimirlem22  33920  poimirlem23  33921  mendvscafval  38545  binomcxplemnn0  39330  xpprsng  42909