Theorem xpeq2 4860

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 2493	. . . 4 |- ( A = B -> ( y e. A <-> y e. B ) )
2	1	anbi2d 708	. . 3 |- ( A = B -> ( ( x e. C /\ y e. A ) <-> ( x e. C /\ y e. B ) ) )
3	2	opabbidv 4480	. 2 |- ( A = B -> { <. x , y >. | ( x e. C /\ y e. A ) } = { <. x , y >. | ( x e. C /\ y e. B ) } )
4		df-xp 4851	. 2 |- ( C X. A ) = { <. x , y >. | ( x e. C /\ y e. A ) }
5		df-xp 4851	. 2 |- ( C X. B ) = { <. x , y >. | ( x e. C /\ y e. B ) }
6	3, 4, 5	3eqtr4g 2486	1 |- ( A = B -> ( C X. A ) = ( C X. B ) )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   e. wcel 1867   {copab 4474   X. cxp 4843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-opab 4476  df-xp 4851

This theorem is referenced by:  xpeq12  4864  xpeq2i  4866  xpeq2d  4869  xpnz  5267  xpdisj2  5270  dmxpss  5279  rnxpid  5281  xpcan  5284  unixp  5380  fconst5  6128  pmvalg  7482  xpcomeng  7661  unxpdom  7776  marypha1  7945  dfac5lem3  8545  dfac5lem4  8546  hsmexlem8  8843  axdc4uz  12182  hashxp  12590  mamufval  19347  txuni2  20517  txbas  20519  txopn  20554  txrest  20583  txdis  20584  txdis1cn  20587  txtube  20592  txcmplem2  20594  tx1stc  20602  qustgplem  21072  tsmsxplem1  21104  isgrpo  25810  vci  26053  isvclem  26082  vcoprnelem  26083  issh  26737  hhssablo  26790  hhssnvt  26792  hhsssh  26796  txomap  28541  tpr2rico  28598  elsx  28896  mbfmcst  28961  br2base  28971  dya2iocnrect  28983  sxbrsigalem5  28990  0rrv  29151  ghomgrplem  30136  dfpo2  30223  elima4  30249  isbnd3  31864  hdmap1fval  35118  csbresgVD  36980