Theorem xpeq2 5129

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

Assertion

Ref	Expression
xpeq2	|- ( A = B -> ( C X. A ) = ( C X. B ) )

Proof of Theorem xpeq2

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

Step	Hyp	Ref	Expression
1		eleq2 2690	. . . 4 |- ( A = B -> ( y e. A <-> y e. B ) )
2	1	anbi2d 740	. . 3 |- ( A = B -> ( ( x e. C /\ y e. A ) <-> ( x e. C /\ y e. B ) ) )
3	2	opabbidv 4716	. 2 |- ( A = B -> { <. x , y >. | ( x e. C /\ y e. A ) } = { <. x , y >. | ( x e. C /\ y e. B ) } )
4		df-xp 5120	. 2 |- ( C X. A ) = { <. x , y >. | ( x e. C /\ y e. A ) }
5		df-xp 5120	. 2 |- ( C X. B ) = { <. x , y >. | ( x e. C /\ y e. B ) }
6	3, 4, 5	3eqtr4g 2681	1 |- ( A = B -> ( C X. A ) = ( C X. B ) )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   {copab 4712   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-opab 4713  df-xp 5120

This theorem is referenced by:  xpeq12  5134  xpeq2i  5136  xpeq2d  5139  xpnz  5553  xpdisj2  5556  dmxpss  5565  rnxpid  5567  xpcan  5570  unixp  5668  fconst5  6471  pmvalg  7868  xpcomeng  8052  unxpdom  8167  marypha1  8340  dfac5lem3  8948  dfac5lem4  8949  hsmexlem8  9246  axdc4uz  12783  hashxp  13221  mamufval  20191  txuni2  21368  txbas  21370  txopn  21405  txrest  21434  txdis  21435  txdis1cn  21438  txtube  21443  txcmplem2  21445  tx1stc  21453  qustgplem  21924  tsmsxplem1  21956  isgrpo  27351  vciOLD  27416  isvclem  27432  issh  28065  hhssablo  28120  hhssnvt  28122  hhsssh  28126  txomap  29901  tpr2rico  29958  elsx  30257  mbfmcst  30321  br2base  30331  dya2iocnrect  30343  sxbrsigalem5  30350  0rrv  30513  dfpo2  31645  elima4  31679  finxpeq1  33223  isbnd3  33583  hdmap1fval  37086  csbresgVD  39131