MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpeq1i Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 xpeq1i.1 . 2 𝐴 = 𝐵
2 xpeq1 5157 . 2 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
31, 2ax-mp 5 1 (𝐴 × 𝐶) = (𝐵 × 𝐶)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator