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

Theorem xpeq1i 5125
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 5118 . 2 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
31, 2ax-mp 5 1 (𝐴 × 𝐶) = (𝐵 × 𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481   × cxp 5102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-opab 4704  df-xp 5110
This theorem is referenced by:  iunxpconst  5165  xpindi  5244  difxp2  5548  resdmres  5613  curry2  7257  mapsnconst  7888  mapsncnv  7889  cda1dif  8983  cdaassen  8989  infcda1  9000  geomulcvg  14588  hofcl  16880  evlsval  19500  matvsca2  20215  ovoliunnul  23256  vitalilem5  23362  lgam1  24771  finxp2o  33207  finxp3o  33208  poimirlem3  33383  poimirlem5  33385  poimirlem10  33390  poimirlem22  33402  poimirlem23  33403  mendvscafval  37579  binomcxplemnn0  38368  xpprsng  41875
  Copyright terms: Public domain W3C validator