Theorem xpeq1i 5024

Description: Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.)

Hypothesis

Ref	Expression
xpeq1i.1

Assertion

Ref	Expression
xpeq1i

Proof of Theorem xpeq1i

Step	Hyp	Ref	Expression
1		xpeq1i.1	. 2
2		xpeq1 5018	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  X.cxp 5002

This theorem is referenced by:  iunxpconst  5061  xpindi  5141  difxp2  5438  resdmres  5503  curry2  6895  mapsnconst  7484  mapsncnv  7485  cda1dif  8577  cdaassen  8583  infcda1  8594  geomulcvg  13685  hofcl  15528  evlsval  18188  matvsca2  18930  ovoliunnul  21918  vitalilem5  22021  lgam1  28606  mendvscafval  31139  binomcxplemnn0  31254  xpprsng  32921

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