Theorem xpeq2 4849

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 2518	. . . 4 |- ( A = B -> ( y e. A <-> y e. B ) )
2	1	anbi2d 710	. . 3 |- ( A = B -> ( ( x e. C /\ y e. A ) <-> ( x e. C /\ y e. B ) ) )
3	2	opabbidv 4466	. 2 |- ( A = B -> { <. x , y >. | ( x e. C /\ y e. A ) } = { <. x , y >. | ( x e. C /\ y e. B ) } )
4		df-xp 4840	. 2 |- ( C X. A ) = { <. x , y >. | ( x e. C /\ y e. A ) }
5		df-xp 4840	. 2 |- ( C X. B ) = { <. x , y >. | ( x e. C /\ y e. B ) }
6	3, 4, 5	3eqtr4g 2510	1 |- ( A = B -> ( C X. A ) = ( C X. B ) )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1444   e. wcel 1887   {copab 4460   X. cxp 4832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-opab 4462  df-xp 4840

This theorem is referenced by:  xpeq12  4853  xpeq2i  4855  xpeq2d  4858  xpnz  5256  xpdisj2  5259  dmxpss  5268  rnxpid  5270  xpcan  5273  unixp  5369  fconst5  6122  pmvalg  7483  xpcomeng  7664  unxpdom  7779  marypha1  7948  dfac5lem3  8556  dfac5lem4  8557  hsmexlem8  8854  axdc4uz  12196  hashxp  12606  mamufval  19410  txuni2  20580  txbas  20582  txopn  20617  txrest  20646  txdis  20647  txdis1cn  20650  txtube  20655  txcmplem2  20657  tx1stc  20665  qustgplem  21135  tsmsxplem1  21167  isgrpo  25924  vci  26167  isvclem  26196  vcoprnelem  26197  issh  26861  hhssablo  26914  hhssnvt  26916  hhsssh  26920  txomap  28661  tpr2rico  28718  elsx  29016  mbfmcst  29081  br2base  29091  dya2iocnrect  29103  sxbrsigalem5  29110  0rrv  29284  ghomgrplem  30307  dfpo2  30395  elima4  30421  finxpeq1  31778  isbnd3  32116  hdmap1fval  35365  csbresgVD  37292