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

Theorem opeq1d 3762
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 3756 . 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 1619   <.cop 3603
This theorem is referenced by:  oteq1  3765  oteq2  3766  opth  4203  cbvoprab2  5839  unxpdomlem1  7021  mulcanenq  8538  ax1rid  8737  axrnegex  8738  fseq1m1p1  10810  uzrdglem  10972  fsum2dlem  12184  ruclem1  12457  imasaddvallem  13379  iscatd2  13531  moni  13587  homadmcd  13822  curf1  13947  curf1cl  13950  curf2  13951  hofcl  13981  gsum2d  15171  imasdsf1olem  17885  ovoliunlem1  18809  cxpcn3  20036  nvi  21116  nvop  21189  phop  21342  br8  23470  axlowdimlem15  23945  axlowdim  23950  fvtransport  24016  eqvinopb  24317  isded  25089  dedi  25090  iscatOLD  25107  cati  25108  cmp2morpcats  25314  cmpmorass  25319  cmpidmor3  25323
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609
  Copyright terms: Public domain W3C validator