MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpeq2 Structured version   Unicode version

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.
StepHypRef Expression
1 eleq2 2493 . . . 4  |-  ( A  =  B  ->  (
y  e.  A  <->  y  e.  B ) )
21anbi2d 708 . . 3  |-  ( A  =  B  ->  (
( x  e.  C  /\  y  e.  A
)  <->  ( x  e.  C  /\  y  e.  B ) ) )
32opabbidv 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 ) }
63, 4, 53eqtr4g 2486 1  |-  ( A  =  B  ->  ( C  X.  A )  =  ( C  X.  B
) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator