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

Theorem xpeq2i 5285
Description: Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.)
Hypothesis
Ref Expression
xpeq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
xpeq2i (𝐶 × 𝐴) = (𝐶 × 𝐵)

Proof of Theorem xpeq2i
StepHypRef Expression
1 xpeq1i.1 . 2 𝐴 = 𝐵
2 xpeq2 5278 . 2 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
31, 2ax-mp 5 1 (𝐶 × 𝐴) = (𝐶 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1624   × cxp 5256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-opab 4857  df-xp 5264
This theorem is referenced by:  xpindir  5404  xpssres  5584  difxp1  5709  xpima  5726  xpexgALT  7318  curry1  7429  fparlem3  7439  fparlem4  7440  xp1en  8203  xp2cda  9186  xpcdaen  9189  pwcda1  9200  pwcdandom  9673  yonedalem3b  17112  yonedalem3  17113  pws1  18808  pwsmgp  18810  xkoinjcn  21684  imasdsf1olem  22371  df0op2  28912  ho01i  28988  nmop0h  29151  mbfmcst  30622  0rrv  30814  cvmlift2lem12  31595  zrdivrng  34057
  Copyright terms: Public domain W3C validator