Theorem xpeq2i 5025

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

Hypothesis

Ref	Expression
xpeq1i.1

Assertion

Ref	Expression
xpeq2i

Proof of Theorem xpeq2i

Step	Hyp	Ref	Expression
1		xpeq1i.1	. 2
2		xpeq2 5019	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  X.cxp 5002

This theorem is referenced by:  xpindir  5142  difxp1  5437  xpima  5454  xpexgALT  6793  curry1  6892  fparlem3  6902  fparlem4  6903  xp1en  7623  xp2cda  8581  xpcdaen  8584  pwcda1  8595  pwcdandom  9066  yonedalem3b  15548  yonedalem3  15549  pws1  17265  pwsmgp  17267  xkoinjcn  20188  imasdsf1olem  20876  zrdivrng  25434  df0op2  26671  ho01i  26747  nmop0h  26910  mbfmcst  28230  0rrv  28390  cvmlift2lem12  28759  xphe  37804

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