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

Theorem xpeq12 5011
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 5006 . 2  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )
2 xpeq2 5007 . 2  |-  ( C  =  D  ->  ( B  X.  C )  =  ( B  X.  D
) )
31, 2sylan9eq 2521 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    X. cxp 4990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-opab 4499  df-xp 4998
This theorem is referenced by:  xpeq12i  5014  xpeq12d  5017  xpid11  5215  xp11  5433  infxpenlem  8380  fpwwe2lem5  9001  pwfseqlem4a  9028  pwfseqlem4  9029  pwfseqlem5  9030  pwfseq  9031  pwsval  14730  mamufval  18647  mvmulfval  18804  txtopon  19820  txbasval  19835  txindislem  19862  ismet  20554  isxmet  20555  ismgm  24984  opidon2  24988  shsval  25892  prdsbnd2  29881  ttac  30571  sblpnf  30782
  Copyright terms: Public domain W3C validator