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

Theorem xpeq1 5003
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 2516 . . . 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 4500 . 2  |-  ( A  =  B  ->  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  C ) }  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  e.  C ) } )
4 df-xp 4995 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
5 df-xp 4995 . 2  |-  ( B  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  C ) }
63, 4, 53eqtr4g 2509 1  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1383    e. wcel 1804   {copab 4494    X. cxp 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-opab 4496  df-xp 4995
This theorem is referenced by:  xpeq12  5008  xpeq1i  5009  xpeq1d  5012  opthprc  5037  dmxpid  5212  reseq2  5258  xpnz  5416  xpdisj1  5418  xpcan2  5434  xpima  5439  unixp  5530  unixpid  5532  pmvalg  7433  xpsneng  7604  xpcomeng  7611  xpdom2g  7615  fodomr  7670  unxpdom  7729  xpfi  7793  marypha1lem  7895  cdaval  8553  iundom2g  8918  hashxplem  12473  ramcl  14529  efgval  16714  frgpval  16755  frlmval  18757  txuni2  20044  txbas  20046  txopn  20081  txrest  20110  txdis  20111  txdis1cn  20114  tx1stc  20129  tmdgsum  20572  qustgplem  20597  isgrpo  25176  hhssablo  26157  hhssnvt  26159  hhsssh  26163  txomap  27815  tpr2rico  27872  elsx  28143  br2base  28218  dya2iocnrect  28230  sxbrsigalem5  28237  sibf0  28254  cvmlift2lem13  28738  ghomgrplem  29007
  Copyright terms: Public domain W3C validator