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

Theorem opeq1d 4208
Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
Hypothesis
Ref Expression
opeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
opeq1d  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  C >. )

Proof of Theorem opeq1d
StepHypRef Expression
1 opeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 opeq1 4202 . 2  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
31, 2syl 16 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  C >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   <.cop 4020
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-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021
This theorem is referenced by:  oteq1  4211  oteq2  4212  opth  4711  cbvoprab2  6355  unxpdomlem1  7726  mulcanenq  9341  ax1rid  9541  axrnegex  9542  fseq1m1p1  11762  uzrdglem  12047  swrd0swrd  12665  swrdccat  12697  swrdccat3a  12698  swrdccat3blem  12699  cshw0  12744  cshwmodn  12745  s2prop  12841  s4prop  12842  fsum2dlem  13564  ruclem1  13841  imasaddvallem  14803  iscatd2  14955  moni  15008  homadmcd  15243  curf1  15368  curf1cl  15371  curf2  15372  hofcl  15402  gsum2dlem2  16872  gsum2dOLD  16874  mat1dimmul  18851  imasdsf1olem  20749  ovoliunlem1  21786  cxpcn3  22994  axlowdimlem15  24131  axlowdim  24136  nvi  25379  nvop  25452  phop  25605  br8d  27335  fgreu  27385  fvproj  27708  mvhfval  28766  mpst123  28773  fprod2dlem  29085  br8  29160  fvtransport  29657
  Copyright terms: Public domain W3C validator