Theorem xpeq2 5014

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 2540	. . . 4 |- ( A = B -> ( y e. A <-> y e. B ) )
2	1	anbi2d 703	. . 3 |- ( A = B -> ( ( x e. C /\ y e. A ) <-> ( x e. C /\ y e. B ) ) )
3	2	opabbidv 4510	. 2 |- ( A = B -> { <. x , y >. | ( x e. C /\ y e. A ) } = { <. x , y >. | ( x e. C /\ y e. B ) } )
4		df-xp 5005	. 2 |- ( C X. A ) = { <. x , y >. | ( x e. C /\ y e. A ) }
5		df-xp 5005	. 2 |- ( C X. B ) = { <. x , y >. | ( x e. C /\ y e. B ) }
6	3, 4, 5	3eqtr4g 2533	1 |- ( A = B -> ( C X. A ) = ( C X. B ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   e. wcel 1767   {copab 4504   X. cxp 4997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-opab 4506  df-xp 5005

This theorem is referenced by:  xpeq12  5018  xpeq2i  5020  xpeq2d  5023  xpnz  5425  xpdisj2  5428  dmxpss  5437  rnxpid  5439  xpcan  5442  unixp  5539  fconst5  6117  pmvalg  7431  xpcomeng  7609  unxpdom  7727  marypha1  7893  dfac5lem3  8505  dfac5lem4  8506  hsmexlem8  8803  axdc4uz  12060  hashxp  12457  mamufval  18670  txuni2  19817  txbas  19819  txopn  19854  txrest  19883  txdis  19884  txdis1cn  19887  txtube  19892  txcmplem2  19894  tx1stc  19902  divstgplem  20370  tsmsxplem1  20406  isgrpo  24890  drngoi  25101  vci  25133  isvclem  25162  vcoprnelem  25163  issh  25817  hhssablo  25871  hhssnvt  25873  hhsssh  25877  txomap  27516  tpr2rico  27546  elsx  27821  mbfmcst  27886  br2base  27896  dya2iocnrect  27908  sxbrsigalem5  27915  0rrv  28046  ghomgrplem  28520  dfpo2  28777  elima4  28802  isbnd3  29899  csbresgVD  32784  hdmap1fval  36603