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

Theorem xpeq1i 5008
Description: Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.)
Hypothesis
Ref Expression
xpeq1i.1  |-  A  =  B
Assertion
Ref Expression
xpeq1i  |-  ( A  X.  C )  =  ( B  X.  C
)

Proof of Theorem xpeq1i
StepHypRef Expression
1 xpeq1i.1 . 2  |-  A  =  B
2 xpeq1 5002 . 2  |-  ( A  =  B  ->  ( A  X.  C )  =  ( B  X.  C
) )
31, 2ax-mp 5 1  |-  ( A  X.  C )  =  ( B  X.  C
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    X. cxp 4986
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-opab 4498  df-xp 4994
This theorem is referenced by:  iunxpconst  5045  xpindi  5125  difxp2  5418  resdmres  5481  curry2  6868  mapsnconst  7457  mapsncnv  7458  cda1dif  8547  cdaassen  8553  infcda1  8564  geomulcvg  13767  hofcl  15727  evlsval  18383  matvsca2  19097  ovoliunnul  22084  vitalilem5  22187  lgam1  28870  mendvscafval  31380  binomcxplemnn0  31495  xpprsng  33175
  Copyright terms: Public domain W3C validator