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

Theorem xpeq12 5094
Description: Equality theorem for Cartesian product. (Contributed by FL, 31-Aug-2009.)
Assertion
Ref Expression
xpeq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))

Proof of Theorem xpeq12
StepHypRef Expression
1 xpeq1 5088 . 2 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
2 xpeq2 5089 . 2 (𝐶 = 𝐷 → (𝐵 × 𝐶) = (𝐵 × 𝐷))
31, 2sylan9eq 2675 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480   × cxp 5072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-opab 4674  df-xp 5080
This theorem is referenced by:  xpeq12i  5097  xpeq12d  5100  xpid11  5307  xp11  5528  infxpenlem  8780  fpwwe2lem5  9400  pwfseqlem4a  9427  pwfseqlem4  9428  pwfseqlem5  9429  pwfseq  9430  pwsval  16067  mamufval  20110  mvmulfval  20267  txtopon  21304  txbasval  21319  txindislem  21346  ismet  22038  isxmet  22039  shsval  28020  prdsbnd2  33226  ismgmOLD  33281  opidon2OLD  33285  ttac  37083  rfovd  37777  fsovrfovd  37785  sblpnf  37991
  Copyright terms: Public domain W3C validator