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

Theorem opeq1d 3977
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 3971 . 2  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
31, 2syl 16 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   <.cop 3804
This theorem is referenced by:  oteq1  3980  oteq2  3981  opth  4422  cbvoprab2  6131  unxpdomlem1  7299  mulcanenq  8821  ax1rid  9020  axrnegex  9021  fseq1m1p1  11106  uzrdglem  11280  s2prop  11844  s4prop  11845  fsum2dlem  12537  ruclem1  12813  imasaddvallem  13737  iscatd2  13889  moni  13945  homadmcd  14180  curf1  14305  curf1cl  14308  curf2  14309  hofcl  14339  gsum2d  15529  imasdsf1olem  18386  ovoliunlem1  19381  cxpcn3  20615  nvi  22076  nvop  22149  phop  22302  fprod2dlem  25288  br8  25363  axlowdimlem15  25838  axlowdim  25843  fvtransport  25909  swrdccatin12b  28069  swrdccat3a  28072  swrdccat3b  28073
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810
  Copyright terms: Public domain W3C validator