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

Theorem opeq12 3798
Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
Assertion
Ref Expression
opeq12  |-  ( ( A  =  C  /\  B  =  D )  -> 
<. A ,  B >.  = 
<. C ,  D >. )

Proof of Theorem opeq12
StepHypRef Expression
1 opeq1 3796 . 2  |-  ( A  =  C  ->  <. A ,  B >.  =  <. C ,  B >. )
2 opeq2 3797 . 2  |-  ( B  =  D  ->  <. C ,  B >.  =  <. C ,  D >. )
31, 2sylan9eq 2335 1  |-  ( ( A  =  C  /\  B  =  D )  -> 
<. A ,  B >.  = 
<. C ,  D >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623   <.cop 3643
This theorem is referenced by:  opeq12i  3801  opeq12d  3804  cbvopab  4087  opth  4245  copsex2t  4253  copsex2g  4254  relop  4834  funopg  5286  fsn  5696  fnressn  5705  cbvoprab12  5920  eqopi  6156  tposoprab  6270  omeu  6583  brecop  6751  th3q  6767  ecovcom  6769  ecovass  6770  ecovdi  6771  xpf1o  7023  addsrpr  8697  addcnsr  8757  axcnre  8786  seqeq1  11049  fsumcnv  12236  eucalgval2  12751  xpstopnlem1  17500  divstgplem  17803  brsegle  24731  cbcpcp  25162  1ded  25738  isntr  25873  islimcat  25876  idmor  25946
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