Theorem xpeq2 5004

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 2516	. . . 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 4500	. 2 |- ( A = B -> { <. x , y >. | ( x e. C /\ y e. A ) } = { <. x , y >. | ( x e. C /\ y e. B ) } )
4		df-xp 4995	. 2 |- ( C X. A ) = { <. x , y >. | ( x e. C /\ y e. A ) }
5		df-xp 4995	. 2 |- ( C X. B ) = { <. x , y >. | ( x e. C /\ y e. B ) }
6	3, 4, 5	3eqtr4g 2509	1 |- ( A = B -> ( C X. A ) = ( C X. B ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1383   e. wcel 1804   {copab 4494   X. cxp 4987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-opab 4496  df-xp 4995

This theorem is referenced by:  xpeq12  5008  xpeq2i  5010  xpeq2d  5013  xpnz  5416  xpdisj2  5419  dmxpss  5428  rnxpid  5430  xpcan  5433  unixp  5530  fconst5  6113  pmvalg  7433  xpcomeng  7611  unxpdom  7729  marypha1  7896  dfac5lem3  8509  dfac5lem4  8510  hsmexlem8  8807  axdc4uz  12072  hashxp  12471  mamufval  18760  txuni2  19939  txbas  19941  txopn  19976  txrest  20005  txdis  20006  txdis1cn  20009  txtube  20014  txcmplem2  20016  tx1stc  20024  qustgplem  20492  tsmsxplem1  20528  isgrpo  25070  vci  25313  isvclem  25342  vcoprnelem  25343  issh  25997  hhssablo  26051  hhssnvt  26053  hhsssh  26057  txomap  27710  tpr2rico  27767  elsx  28038  mbfmcst  28103  br2base  28113  dya2iocnrect  28125  sxbrsigalem5  28132  0rrv  28263  ghomgrplem  28902  dfpo2  29159  elima4  29184  isbnd3  30255  csbresgVD  33423  hdmap1fval  37258