Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  xpeq1 Unicode version

Theorem xpeq1 4562
 Description: Equality theorem for cross product. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
xpeq1

Proof of Theorem xpeq1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq2 2204 . . . 4
21anbi1d 461 . . 3
32opabbidv 4003 . 2
4 df-xp 4554 . 2
5 df-xp 4554 . 2
63, 4, 53eqtr4g 2198 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wceq 1332   wcel 1481  copab 3997   cxp 4546 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-opab 3999  df-xp 4554 This theorem is referenced by:  xpeq12  4567  xpeq1i  4568  xpeq1d  4571  opthprc  4599  reseq2  4823  xpeq0r  4970  xpdisj1  4972  xpima1  4994  pmvalg  6562  xpsneng  6725  xpcomeng  6731  xpdom2g  6735  xpfi  6828  exmidomni  7024  exmidfodomrlemim  7077  hashxp  10624  txuni2  12484  txbas  12486  txopn  12493  txrest  12504  txdis  12505  txdis1cn  12506  xmettxlem  12737  xmettx  12738
 Copyright terms: Public domain W3C validator