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

Theorem xpeq1 4875
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 2504 . . . 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 4376 . 2  |-  ( A  =  B  ->  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  C ) }  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  e.  C ) } )
4 df-xp 4867 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
5 df-xp 4867 . 2  |-  ( B  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  C ) }
63, 4, 53eqtr4g 2500 1  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   {copab 4370    X. cxp 4859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-opab 4372  df-xp 4867
This theorem is referenced by:  xpeq12  4880  xpeq1i  4881  xpeq1d  4884  opthprc  4907  dmxpid  5080  reseq2  5126  xpnz  5278  xpdisj1  5280  xpcan2  5296  xpima  5301  unixp  5391  unixpid  5393  pmvalg  7246  xpsneng  7417  xpcomeng  7424  xpdom2g  7428  fodomr  7483  unxpdom  7541  xpfi  7604  marypha1lem  7704  cdaval  8360  iundom2g  8725  hashxplem  12216  ramcl  14111  efgval  16235  frgpval  16276  frlmval  18195  txuni2  19160  txbas  19162  txopn  19197  txrest  19226  txdis  19227  txdis1cn  19230  tx1stc  19245  tmdgsum  19688  divstgplem  19713  isgrpo  23705  drngoi  23916  hhssablo  24686  hhssnvt  24688  hhsssh  24692  tpr2rico  26364  elsx  26630  br2base  26706  dya2iocnrect  26718  sxbrsigalem5  26725  sibf0  26742  cvmlift2lem13  27226  ghomgrplem  27330
  Copyright terms: Public domain W3C validator