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

Theorem opeq12 3814
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 3812 . 2  |-  ( A  =  C  ->  <. A ,  B >.  =  <. C ,  B >. )
2 opeq2 3813 . 2  |-  ( B  =  D  ->  <. C ,  B >.  =  <. C ,  D >. )
31, 2sylan9eq 2348 1  |-  ( ( A  =  C  /\  B  =  D )  -> 
<. A ,  B >.  = 
<. C ,  D >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632   <.cop 3656
This theorem is referenced by:  opeq12i  3817  opeq12d  3820  cbvopab  4103  opth  4261  copsex2t  4269  copsex2g  4270  relop  4850  funopg  5302  fsn  5712  fnressn  5721  cbvoprab12  5936  eqopi  6172  tposoprab  6286  omeu  6599  brecop  6767  th3q  6783  ecovcom  6785  ecovass  6786  ecovdi  6787  xpf1o  7039  addsrpr  8713  addcnsr  8773  axcnre  8802  seqeq1  11065  fsumcnv  12252  eucalgval2  12767  xpstopnlem1  17516  divstgplem  17819  brsegle  24803  cbcpcp  25265  1ded  25841  isntr  25976  islimcat  25979  idmor  26049
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