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

Theorem opeq1d 3804
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 3798 . 2  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
31, 2syl 17 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1624   <.cop 3645
This theorem is referenced by:  oteq1  3807  oteq2  3808  opth  4245  cbvoprab2  5881  unxpdomlem1  7063  mulcanenq  8580  ax1rid  8779  axrnegex  8780  fseq1m1p1  10853  uzrdglem  11015  fsum2dlem  12228  ruclem1  12504  imasaddvallem  13426  iscatd2  13578  moni  13634  homadmcd  13869  curf1  13994  curf1cl  13997  curf2  13998  hofcl  14028  gsum2d  15218  imasdsf1olem  17932  ovoliunlem1  18856  cxpcn3  20083  nvi  21163  nvop  21236  phop  21389  br8  23517  axlowdimlem15  23992  axlowdim  23997  fvtransport  24063  eqvinopb  24364  isded  25136  dedi  25137  iscatOLD  25154  cati  25155  cmp2morpcats  25361  cmpmorass  25366  cmpidmor3  25370
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651
  Copyright terms: Public domain W3C validator