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

Theorem xpeq12d 5029
Description: Equality deduction for Cartesian product. (Contributed by NM, 8-Dec-2013.)
Hypotheses
Ref Expression
xpeq1d.1
xpeq12d.2
Assertion
Ref Expression
xpeq12d

Proof of Theorem xpeq12d
StepHypRef Expression
1 xpeq1d.1 . 2
2 xpeq12d.2 . 2
3 xpeq12 5023 . 2
41, 2, 3syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  X.cxp 5002
This theorem is referenced by:  sqxpeqd  5030  opeliunxp  5056  mpt2mptsx  6863  dmmpt2ssx  6865  fmpt2x  6866  ovmptss  6881  fparlem3  6902  fparlem4  6903  erssxp  7353  marypha2lem2  7916  ackbij1lem8  8628  r1om  8645  fictb  8646  axcc2lem  8837  axcc2  8838  axdc4lem  8856  fsum2dlem  13585  fsumcom2  13589  ackbijnn  13640  fprod2dlem  13784  fprodcom2  13788  homaval  15358  xpcval  15446  xpchom  15449  xpchom2  15455  1stfval  15460  2ndfval  15463  xpcpropd  15477  evlfval  15486  isga  16329  symgval  16404  gsumcom2  17003  gsumxp  17004  gsumxpOLD  17006  ablfaclem3  17138  psrval  18011  mamufval  18887  mamudm  18890  mvmulfval  19044  mavmuldm  19052  mavmul0g  19055  txbas  20068  ptbasfi  20082  txindis  20135  tmsxps  21039  metuvalOLD  21052  metustexhalfOLD  21066  metustexhalf  21067  is2wlkonot  24863  is2spthonot  24864  2wlksot  24867  2spthsot  24868  2wlkonot3v  24875  2spthonot3v  24876  cvmliftlem15  28743  mexval  28862  mpstval  28895  mclsval  28923  mclsax  28929  mclsppslem  28943  filnetlem4  30199  heiborlem3  30309  opeliun2xp  32922  dmmpt2ssx2  32926  dvhfset  36807  dvhset  36808  dibffval  36867  dibfval  36868  hdmap1fval  37524
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