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

Theorem xpeq1 4837
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 2475 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21anbi1d 703 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  /\  y  e.  C
)  <->  ( x  e.  B  /\  y  e.  C ) ) )
32opabbidv 4458 . 2  |-  ( A  =  B  ->  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  C ) }  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  e.  C ) } )
4 df-xp 4829 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
5 df-xp 4829 . 2  |-  ( B  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  C ) }
63, 4, 53eqtr4g 2468 1  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    e. wcel 1842   {copab 4452    X. cxp 4821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-opab 4454  df-xp 4829
This theorem is referenced by:  xpeq12  4842  xpeq1i  4843  xpeq1d  4846  opthprc  4871  dmxpid  5043  reseq2  5089  xpnz  5244  xpdisj1  5246  xpcan2  5262  xpima  5267  unixp  5357  unixpid  5359  pmvalg  7468  xpsneng  7640  xpcomeng  7647  xpdom2g  7651  fodomr  7706  unxpdom  7762  xpfi  7825  marypha1lem  7927  cdaval  8582  iundom2g  8947  hashxplem  12540  dmtrclfv  13001  ramcl  14756  efgval  17059  frgpval  17100  frlmval  19077  txuni2  20358  txbas  20360  txopn  20395  txrest  20424  txdis  20425  txdis1cn  20428  tx1stc  20443  tmdgsum  20886  qustgplem  20911  isgrpo  25612  hhssablo  26593  hhssnvt  26595  hhsssh  26599  txomap  28290  tpr2rico  28347  elsx  28642  br2base  28717  dya2iocnrect  28729  sxbrsigalem5  28736  sibf0  28782  cvmlift2lem13  29612  ghomgrplem  29881
  Copyright terms: Public domain W3C validator