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

Theorem opeq1d 3818
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 3812 . 2  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
31, 2syl 15 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   <.cop 3656
This theorem is referenced by:  oteq1  3821  oteq2  3822  opth  4261  cbvoprab2  5935  unxpdomlem1  7083  mulcanenq  8600  ax1rid  8799  axrnegex  8800  fseq1m1p1  10874  uzrdglem  11036  fsum2dlem  12249  ruclem1  12525  imasaddvallem  13447  iscatd2  13599  moni  13655  homadmcd  13890  curf1  14015  curf1cl  14018  curf2  14019  hofcl  14049  gsum2d  15239  imasdsf1olem  17953  ovoliunlem1  18877  cxpcn3  20104  nvi  21186  nvop  21259  phop  21412  isibfm  23608  rrvmbfm  23660  br8  24184  axlowdimlem15  24656  axlowdim  24661  fvtransport  24727  eqvinopb  25068  isded  25839  dedi  25840  iscatOLD  25857  cati  25858  cmp2morpcats  26064  cmpmorass  26069  cmpidmor3  26073  s2prop  28221  s4prop  28222
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662
  Copyright terms: Public domain W3C validator