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

Theorem xpeq12 4869
Description: Equality theorem for Cartesian product. (Contributed by FL, 31-Aug-2009.)
Assertion
Ref Expression
xpeq12  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )

Proof of Theorem xpeq12
StepHypRef Expression
1 xpeq1 4864 . 2  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )
2 xpeq2 4865 . 2  |-  ( C  =  D  ->  ( B  X.  C )  =  ( B  X.  D
) )
31, 2sylan9eq 2483 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    X. cxp 4848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-opab 4480  df-xp 4856
This theorem is referenced by:  xpeq12i  4872  xpeq12d  4875  xpid11  5072  xp11  5288  infxpenlem  8446  fpwwe2lem5  9060  pwfseqlem4a  9087  pwfseqlem4  9088  pwfseqlem5  9089  pwfseq  9090  pwsval  15372  mamufval  19397  mvmulfval  19554  txtopon  20593  txbasval  20608  txindislem  20635  ismet  21325  isxmet  21326  ismgmOLD  26034  opidon2OLD  26038  shsval  26951  prdsbnd2  32041  ttac  35811  sblpnf  36516
  Copyright terms: Public domain W3C validator