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

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