Theorem xpeq1d 5027

Description: Equality deduction for Cartesian product. (Contributed by Jeff Madsen, 17-Jun-2010.)

Hypothesis

Ref	Expression
xpeq1d.1

Assertion

Ref	Expression
xpeq1d

Proof of Theorem xpeq1d

Step	Hyp	Ref	Expression
1		xpeq1d.1	. 2
2		xpeq1 5018	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  =wceq 1395  X.cxp 5002

This theorem is referenced by:  csbres  5281  xpssres  5313  curry1  6892  fparlem3  6902  fparlem4  6903  ixpsnf1o  7529  xpfi  7811  dfac5lem3  8527  dfac5lem4  8528  cdaassen  8583  hashxplem  12491  repsw1  12755  subgga  16338  gasubg  16340  sylow2blem2  16641  psrval  18011  mpfrcl  18187  evlsval  18188  mamufval  18887  mat1dimscm  18977  mdetunilem3  19116  mdetunilem4  19117  mdetunilem9  19122  txindislem  20134  txtube  20141  txcmplem1  20142  txhaus  20148  xkoinjcn  20188  pt1hmeo  20307  tsmsxplem1  20655  tsmsxplem2  20656  cnmpt2pc  21428  dchrval  23509  axlowdimlem15  24259  axlowdim  24264  0ofval  25702  esumcvg  28092  sxbrsigalem0  28242  sxbrsigalem3  28243  sxbrsigalem2  28257  ofcccat  28498  mexval2  28863  sdclem1  30236  ismrer1  30334  mzpclval  30657  mendval  31132  ldualset  34850  dibval  36869  dibval3N  36873  dib0  36891  dihwN  37016  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