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 2518 1  |-  ( ( A  =  C  /\  B  =  D )  -> 
<. A ,  B >.  = 
<. C ,  D >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1395   <.cop 4038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039
This theorem is referenced by:  opeq12i  4224  opeq12d  4227  cbvopab  4525  opth  4730  copsex2t  4743  copsex2g  4744  relop  5163  funopg  5626  fvn0ssdmfun  6023  fsn  6070  fnressn  6084  fmptsng  6093  fmptsnd  6094  tpres  6125  cbvoprab12  6370  eqopi  6833  f1o2ndf1  6907  tposoprab  7009  omeu  7252  brecop  7422  ecovcom  7435  ecovass  7436  ecovdi  7437  xpf1o  7698  addsrmo  9467  mulsrmo  9468  addsrpr  9469  mulsrpr  9470  addcnsr  9529  axcnre  9558  seqeq1  12112  fsumcnv  13599  fprodcnv  13798  eucalgval2  14221  xpstopnlem1  20435  qustgplem  20744  isrusgra  25053  brabgaf  27599  qqhval2  28116  brsegle  29920  dvnprodlem1  31904
  Copyright terms: Public domain W3C validator