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

Theorem xpeq12 5023
 Description: Equality theorem for Cartesian product. (Contributed by FL, 31-Aug-2009.)
Assertion
Ref Expression
xpeq12

Proof of Theorem xpeq12
StepHypRef Expression
1 xpeq1 5018 . 2
2 xpeq2 5019 . 2
31, 2sylan9eq 2518 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  X.cxp 5002 This theorem is referenced by:  xpeq12i  5026  xpeq12d  5029  xpid11  5229  xp11  5447  infxpenlem  8412  fpwwe2lem5  9033  pwfseqlem4a  9060  pwfseqlem4  9061  pwfseqlem5  9062  pwfseq  9063  pwsval  14883  mamufval  18887  mvmulfval  19044  txtopon  20092  txbasval  20107  txindislem  20134  ismet  20826  isxmet  20827  ismgmOLD  25322  opidon2OLD  25326  shsval  26230  prdsbnd2  30291  ttac  30978  sblpnf  31190 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-opab 4511  df-xp 5010
 Copyright terms: Public domain W3C validator