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

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

Proof of Theorem xpeq12
StepHypRef Expression
1 xpeq1 5327 . 2 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
2 xpeq2 5334 . 2 (𝐶 = 𝐷 → (𝐵 × 𝐶) = (𝐵 × 𝐷))
31, 2sylan9eq 2854 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385   = wceq 1653   × cxp 5311
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 2778
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 2787  df-cleq 2793  df-clel 2796  df-opab 4907  df-xp 5319
This theorem is referenced by:  xpeq12i  5341  xpeq12d  5344  xpid11  5551  xp11  5787  infxpenlem  9123  fpwwe2lem5  9745  pwfseqlem4a  9772  pwfseqlem4  9773  pwfseqlem5  9774  pwfseq  9775  pwsval  16460  mamufval  20515  mvmulfval  20673  txtopon  21722  txbasval  21737  txindislem  21764  ismet  22455  isxmet  22456  shsval  28695  prdsbnd2  34080  ismgmOLD  34135  opidon2OLD  34139  ttac  38383  rfovd  39072  fsovrfovd  39080  sblpnf  39286
  Copyright terms: Public domain W3C validator