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

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
StepHypRef Expression
1 xpeq1i.1 . 2
2 xpeq2 5019 . 2
31, 2ax-mp 5 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator