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

Theorem opeq12i 3801
Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
Hypotheses
Ref Expression
opeq1i.1  |-  A  =  B
opeq12i.2  |-  C  =  D
Assertion
Ref Expression
opeq12i  |-  <. A ,  C >.  =  <. B ,  D >.

Proof of Theorem opeq12i
StepHypRef Expression
1 opeq1i.1 . 2  |-  A  =  B
2 opeq12i.2 . 2  |-  C  =  D
3 opeq12 3798 . 2  |-  ( ( A  =  B  /\  C  =  D )  -> 
<. A ,  C >.  = 
<. B ,  D >. )
41, 2, 3mp2an 653 1  |-  <. A ,  C >.  =  <. B ,  D >.
Colors of variables: wff set class
Syntax hints:    = wceq 1623   <.cop 3643
This theorem is referenced by:  elxp6  6151  addcompq  8574  mulcompq  8576  addassnq  8582  mulassnq  8583  distrnq  8585  1lt2nq  8597  axi2m1  8781  om2uzrdg  11019  rngoi  21047  nvop2  21164  nvvop  21165  phop  21396  hhsssh  21846  axlowdimlem6  23986  dedalg  25155  catded  25176  isdrngo1  25999
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649
  Copyright terms: Public domain W3C validator