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

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

Proof of Theorem xpeq12
StepHypRef Expression
1 xpeq1 5698 . 2 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
2 xpeq2 5705 . 2 (𝐶 = 𝐷 → (𝐵 × 𝐶) = (𝐵 × 𝐷))
31, 2sylan9eq 2796 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1539   × cxp 5682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-opab 5205  df-xp 5690
This theorem is referenced by:  xpeq12i  5712  xpeq12d  5715  xpid11  5942  xp11  6194  infxpenlem  10054  pwfseqlem4a  10702  pwfseqlem4  10703  pwfseqlem5  10704  pwfseq  10705  pwsval  17532  mamufval  22397  mvmulfval  22549  txtopon  23600  txbasval  23615  txindislem  23642  ismet  24334  isxmet  24335  shsval  31332  sat1el2xp  35385  bj-imdirvallem  37182  prdsbnd2  37803  ismgmOLD  37858  opidon2OLD  37862  ttac  43053  rfovd  44019  fsovrfovd  44027  sblpnf  44334
  Copyright terms: Public domain W3C validator