Theorem xpeq2 5019

Description: Equality theorem for Cartesian product. (Contributed by NM, 5-Jul-1994.)

Assertion

Ref	Expression
xpeq2

Proof of Theorem xpeq2

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2530	. . . 4
2	1	anbi2d 703	. . 3
3	2	opabbidv 4515	. 2
4		df-xp 5010	. 2
5		df-xp 5010	. 2
6	3, 4, 5	3eqtr4g 2523	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  {copab 4509  X.cxp 5002

This theorem is referenced by:  xpeq12  5023  xpeq2i  5025  xpeq2d  5028  xpnz  5431  xpdisj2  5434  dmxpss  5443  rnxpid  5445  xpcan  5448  unixp  5545  fconst5  6128  pmvalg  7450  xpcomeng  7629  unxpdom  7747  marypha1  7914  dfac5lem3  8527  dfac5lem4  8528  hsmexlem8  8825  axdc4uz  12093  hashxp  12492  mamufval  18887  txuni2  20066  txbas  20068  txopn  20103  txrest  20132  txdis  20133  txdis1cn  20136  txtube  20141  txcmplem2  20143  tx1stc  20151  qustgplem  20619  tsmsxplem1  20655  isgrpo  25198  vci  25441  isvclem  25470  vcoprnelem  25471  issh  26125  hhssablo  26179  hhssnvt  26181  hhsssh  26185  txomap  27837  tpr2rico  27894  elsx  28165  mbfmcst  28230  br2base  28240  dya2iocnrect  28252  sxbrsigalem5  28259  0rrv  28390  ghomgrplem  29029  dfpo2  29184  elima4  29209  isbnd3  30280  csbresgVD  33695  hdmap1fval  37524

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