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

Theorem xpeq1 5018
Description: Equality theorem for Cartesian 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 2530 . . . 4
21anbi1d 704 . . 3
32opabbidv 4515 . 2
4 df-xp 5010 . 2
5 df-xp 5010 . 2
63, 4, 53eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  {copab 4509  X.cxp 5002
This theorem is referenced by:  xpeq12  5023  xpeq1i  5024  xpeq1d  5027  opthprc  5052  dmxpid  5227  reseq2  5273  xpnz  5431  xpdisj1  5433  xpcan2  5449  xpima  5454  unixp  5545  unixpid  5547  pmvalg  7450  xpsneng  7622  xpcomeng  7629  xpdom2g  7633  fodomr  7688  unxpdom  7747  xpfi  7811  marypha1lem  7913  cdaval  8571  iundom2g  8936  hashxplem  12491  ramcl  14547  efgval  16735  frgpval  16776  frlmval  18779  txuni2  20066  txbas  20068  txopn  20103  txrest  20132  txdis  20133  txdis1cn  20136  tx1stc  20151  tmdgsum  20594  qustgplem  20619  isgrpo  25198  hhssablo  26179  hhssnvt  26181  hhsssh  26185  txomap  27837  tpr2rico  27894  elsx  28165  br2base  28240  dya2iocnrect  28252  sxbrsigalem5  28259  sibf0  28276  cvmlift2lem13  28760  ghomgrplem  29029
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