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

Theorem xpeq12 4842
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 4837 . 2  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )
2 xpeq2 4838 . 2  |-  ( C  =  D  ->  ( B  X.  C )  =  ( B  X.  D
) )
31, 2sylan9eq 2463 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  X.  C
)  =  ( B  X.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    X. cxp 4821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-opab 4454  df-xp 4829
This theorem is referenced by:  xpeq12i  4845  xpeq12d  4848  xpid11  5045  xp11  5260  infxpenlem  8423  fpwwe2lem5  9042  pwfseqlem4a  9069  pwfseqlem4  9070  pwfseqlem5  9071  pwfseq  9072  pwsval  15100  mamufval  19179  mvmulfval  19336  txtopon  20384  txbasval  20399  txindislem  20426  ismet  21118  isxmet  21119  ismgmOLD  25736  opidon2OLD  25740  shsval  26644  prdsbnd2  31573  ttac  35340  sblpnf  36038
  Copyright terms: Public domain W3C validator