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

Theorem opeq1d 4209
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 4203 . 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 1398   <.cop 4022
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-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023
This theorem is referenced by:  oteq1  4212  oteq2  4213  opth  4711  cbvoprab2  6343  unxpdomlem1  7717  mulcanenq  9327  ax1rid  9527  axrnegex  9528  fseq1m1p1  11757  uzrdglem  12050  swrd0swrd  12677  swrdccat  12709  swrdccat3a  12710  swrdccat3blem  12711  cshw0  12756  cshwmodn  12757  s2prop  12853  s4prop  12854  fsum2dlem  13667  fprod2dlem  13866  ruclem1  14048  imasaddvallem  15018  iscatd2  15170  moni  15224  homadmcd  15520  curf1  15693  curf1cl  15696  curf2  15697  hofcl  15727  gsum2dlem2  17194  gsum2dOLD  17196  mat1dimmul  19145  imasdsf1olem  21042  ovoliunlem1  22079  cxpcn3  23290  axlowdimlem15  24461  axlowdim  24466  nvi  25705  nvop  25778  phop  25931  br8d  27678  fgreu  27740  1stpreimas  27752  fvproj  28070  mvhfval  29157  mpst123  29164  br8  29426  fvtransport  29910
  Copyright terms: Public domain W3C validator