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

Theorem xpeq1i 5580
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 5568 . 2 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
31, 2ax-mp 5 1 (𝐴 × 𝐶) = (𝐵 × 𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533   × cxp 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-opab 5128  df-xp 5560
This theorem is referenced by:  iunxpconst  5623  xpindi  5703  difxp2  6022  resdmres  6088  xpprsng  6901  curry2  7801  mapsnconst  8455  mapsncnv  8456  xp2dju  9601  pwdju1  9615  pwdjundom  10088  geomulcvg  15231  hofcl  17508  evlsval  20298  matvsca2  21036  ehl0  24019  ovoliunnul  24107  vitalilem5  24212  lgam1  25640  finxp2o  34679  finxp3o  34680  poimirlem3  34894  poimirlem5  34896  poimirlem10  34901  poimirlem22  34913  poimirlem23  34914  mendvscafval  39788  binomcxplemnn0  40679  itscnhlinecirc02plem3  44770  inlinecirc02p  44773
  Copyright terms: Public domain W3C validator