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

Theorem opeq12 4221
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 4219 . 2  |-  ( A  =  C  ->  <. A ,  B >.  =  <. C ,  B >. )
2 opeq2 4220 . 2  |-  ( B  =  D  ->  <. C ,  B >.  =  <. C ,  D >. )
31, 2sylan9eq 2528 1  |-  ( ( A  =  C  /\  B  =  D )  -> 
<. A ,  B >.  = 
<. C ,  D >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379   <.cop 4039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040
This theorem is referenced by:  opeq12i  4224  opeq12d  4227  cbvopab  4521  opth  4727  copsex2t  4740  copsex2g  4741  relop  5159  funopg  5626  fvn0ssdmfun  6023  fsn  6070  fnressn  6084  fmptsng  6093  fmptsnd  6094  cbvoprab12  6366  eqopi  6829  f1o2ndf1  6903  tposoprab  7003  omeu  7246  brecop  7416  ecovcom  7429  ecovass  7430  ecovdi  7431  xpf1o  7691  addsrmo  9462  mulsrmo  9463  addsrpr  9464  mulsrpr  9465  addcnsr  9524  axcnre  9553  seqeq1  12090  fsumcnv  13568  eucalgval2  14086  xpstopnlem1  20178  qustgplem  20487  isrusgra  24750  qqhval2  27788  fprodcnv  29040  brsegle  29685
  Copyright terms: Public domain W3C validator