Theorem xpeq2 4855

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   {copab 4349   X. cxp 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-opab 4351  df-xp 4846

This theorem is referenced by:  xpeq12  4859  xpeq2i  4861  xpeq2d  4864  xpnz  5257  xpdisj2  5260  dmxpss  5269  rnxpid  5271  xpcan  5274  unixp  5370  fconst5  5935  pmvalg  7225  xpcomeng  7403  unxpdom  7520  marypha1  7684  dfac5lem3  8295  dfac5lem4  8296  hsmexlem8  8593  axdc4uz  11805  hashxp  12196  mamufval  18283  txuni2  19138  txbas  19140  txopn  19175  txrest  19204  txdis  19205  txdis1cn  19208  txtube  19213  txcmplem2  19215  tx1stc  19223  divstgplem  19691  tsmsxplem1  19727  isgrpo  23683  drngoi  23894  vci  23926  isvclem  23955  vcoprnelem  23956  issh  24610  hhssablo  24664  hhssnvt  24666  hhsssh  24670  tpr2rico  26342  elsx  26608  mbfmcst  26674  br2base  26684  dya2iocnrect  26696  sxbrsigalem5  26703  0rrv  26834  ghomgrplem  27308  dfpo2  27565  elima4  27590  isbnd3  28683  csbresgVD  31631  hdmap1fval  35442