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

Theorem xpeq1 4864
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 2495 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21anbi1d 709 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  /\  y  e.  C
)  <->  ( x  e.  B  /\  y  e.  C ) ) )
32opabbidv 4484 . 2  |-  ( A  =  B  ->  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  C ) }  =  { <. x ,  y >.  |  ( x  e.  B  /\  y  e.  C ) } )
4 df-xp 4856 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
5 df-xp 4856 . 2  |-  ( B  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  C ) }
63, 4, 53eqtr4g 2488 1  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1868   {copab 4478    X. cxp 4848
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 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
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 2408  df-cleq 2414  df-clel 2417  df-opab 4480  df-xp 4856
This theorem is referenced by:  xpeq12  4869  xpeq1i  4870  xpeq1d  4873  opthprc  4898  dmxpid  5070  reseq2  5116  xpnz  5272  xpdisj1  5274  xpcan2  5290  xpima  5295  unixp  5385  unixpid  5387  pmvalg  7488  xpsneng  7660  xpcomeng  7667  xpdom2g  7671  fodomr  7726  unxpdom  7782  xpfi  7845  marypha1lem  7950  cdaval  8601  iundom2g  8966  hashxplem  12603  dmtrclfv  13071  ramcl  14975  efgval  17355  frgpval  17396  frlmval  19298  txuni2  20567  txbas  20569  txopn  20604  txrest  20633  txdis  20634  txdis1cn  20637  tx1stc  20652  tmdgsum  21097  qustgplem  21122  isgrpo  25910  hhssablo  26900  hhssnvt  26902  hhsssh  26906  txomap  28657  tpr2rico  28714  elsx  29012  br2base  29087  dya2iocnrect  29099  sxbrsigalem5  29106  sibf0  29163  cvmlift2lem13  30034  ghomgrplem  30303
  Copyright terms: Public domain W3C validator