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

Theorem xpeq1 5013
Description: Equality theorem for Cartesian product. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
xpeq1  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )

Proof of Theorem xpeq1
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq2 2540 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21anbi1d 704 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  /\  y  e.  C
)  <->  ( x  e.  B  /\  y  e.  C ) ) )
32opabbidv 4510 . 2  |-  ( A  =  B  ->  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  C ) }  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  e.  C ) } )
4 df-xp 5005 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
5 df-xp 5005 . 2  |-  ( B  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  C ) }
63, 4, 53eqtr4g 2533 1  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379    e. wcel 1767   {copab 4504    X. cxp 4997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-opab 4506  df-xp 5005
This theorem is referenced by:  xpeq12  5018  xpeq1i  5019  xpeq1d  5022  opthprc  5047  dmxpid  5222  reseq2  5268  xpnz  5426  xpdisj1  5428  xpcan2  5444  xpima  5449  unixp  5540  unixpid  5542  pmvalg  7431  xpsneng  7602  xpcomeng  7609  xpdom2g  7613  fodomr  7668  unxpdom  7727  xpfi  7791  marypha1lem  7893  cdaval  8550  iundom2g  8915  hashxplem  12457  ramcl  14406  efgval  16541  frgpval  16582  frlmval  18574  txuni2  19829  txbas  19831  txopn  19866  txrest  19895  txdis  19896  txdis1cn  19899  tx1stc  19914  tmdgsum  20357  divstgplem  20382  isgrpo  24902  drngoi  25113  hhssablo  25883  hhssnvt  25885  hhsssh  25889  txomap  27528  tpr2rico  27558  elsx  27833  br2base  27908  dya2iocnrect  27920  sxbrsigalem5  27927  sibf0  27944  cvmlift2lem13  28428  ghomgrplem  28532
  Copyright terms: Public domain W3C validator