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

Theorem opeq12d 4210
Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Hypotheses
Ref Expression
opeq1d.1  |-  ( ph  ->  A  =  B )
opeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
opeq12d  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )

Proof of Theorem opeq12d
StepHypRef Expression
1 opeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 opeq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 opeq12 4204 . 2  |-  ( ( A  =  B  /\  C  =  D )  -> 
<. A ,  C >.  = 
<. B ,  D >. )
41, 2, 3syl2anc 661 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   <.cop 4020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021
This theorem is referenced by:  nfopd  4219  csbopg  4220  moop2  4732  fnprb  6114  fliftfuns  6197  dfmpt2  6875  fsplit  6890  fnwelem  6900  seqomlem0  7116  seqomlem1  7117  seqomlem4  7120  qliftfuns  7400  xpassen  7613  xpdom2  7614  xpf1o  7681  xpmapenlem  7686  xpmapen  7687  mapunen  7688  xpwdomg  8014  fseqenlem2  8409  nqereu  9310  addpipq2  9317  addpipq  9318  mulpipq2  9320  mulpipq  9321  1nqenq  9343  mulidnq  9344  ltexnq  9356  prlem934  9414  addsrmo  9453  mulsrmo  9454  addsrpr  9455  mulsrpr  9456  mulcnsr  9516  mulresr  9519  axcnre  9544  om2uzrdg  12049  uzrdgsuci  12053  2swrd1eqwrdeq  12661  swrdswrd0  12669  ccatopth  12677  swrdccatin2d  12707  splval  12709  splcl  12710  cshfn  12743  repswcshw  12762  2swrd2eqwrdeq  12873  ruclem1  13946  eucalgval2  14192  qnumdenbi  14259  crt  14290  phimullem  14291  prmreclem3  14418  imasval  14890  imasaddvallem  14908  xpsff1o  14947  catidex  15053  cidval  15056  catcocl  15064  catass  15065  oppccofval  15093  sectfval  15128  subccocl  15193  isfunc  15212  funcco  15219  idfuval  15224  idfucl  15229  cofuval  15230  cofuval2  15235  cofucl  15236  cofuass  15237  cofulid  15238  cofurid  15239  resfval  15240  resfval2  15241  funcres  15244  isnat  15295  nati  15303  fucco  15310  fuccoval  15311  coaval  15374  catcisolem  15412  xpcval  15425  xpcco  15431  xpcco2  15435  xpccatid  15436  xpcid  15437  1stfval  15439  2ndfval  15442  1stfcl  15445  2ndfcl  15446  prfval  15447  prf1  15448  prf2fval  15449  prf2  15450  prfcl  15451  prf1st  15452  prf2nd  15453  1st2ndprf  15454  xpcpropd  15456  evlfval  15465  evlf2  15466  evlfcllem  15469  evlfcl  15470  curfval  15471  curf1  15473  curf1cl  15476  curf2cl  15479  curfcl  15480  curfpropd  15481  uncf1  15484  uncf2  15485  curfuncf  15486  uncfcurf  15487  diagval  15488  curf2ndf  15495  hofval  15500  hof2fval  15503  hofcl  15507  yonval  15509  hofpropd  15515  yonedalem21  15521  yonedalem22  15526  yonedalem3  15528  symg2bas  16402  mat1dimmul  18956  txcnp  20099  upxp  20102  uptx  20104  hauseqlcld  20125  txlm  20127  txkgen  20131  cnmpt1t  20144  cnmpt2t  20152  txhmeo  20282  pt1hmeo  20285  flfcnp2  20486  ucnimalem  20761  ucnima  20762  fmucndlem  20772  fmucnd  20773  cnheiborlem  21432  pi1xfrcnvlem  21534  ovollb2lem  21877  ovollb2  21878  ovolshftlem2  21899  ovolscalem2  21903  ioombl1  21950  ioorf  21960  ioorval  21961  ioorinv2  21962  uniioombllem6  21975  dyadval  21979  opnmbl  21989  mbfimaopnlem  22040  limccnp2  22274  dvdsmulf1o  23448  ebtwntg  24263  usgrac  24329  numclwlk1lem2fv  25071  numclwlk1lem2fo  25073  hhssnvt  26159  hhsssh  26163  opfv  27464  xppreima  27465  ofpreima  27485  fgreu  27491  fimaproj  27814  qtophaus  27817  qqhval2  27941  rrvadd  28369  erdszelem9  28621  erdszelem10  28622  txpcon  28655  txsconlem  28663  msubval  28863  msubco  28869  mvhval  28872  msubvrs  28898  opnmbllem0  30026  mblfinlem1  30027  mblfinlem2  30028  heiborlem6  30288  heiborlem7  30289  heiborlem8  30290  pellexlem3  30743  pellex  30747  dvnprodlem1  31697  dvnprodlem3  31699  etransclem44  32015  aoveq123d  32217  ressval3d  32509  inclfusubc  32517  funcrngcsetc  32681  funcrngcsetcALT  32682  funcringcsetc  32715  bnj1442  33973  bnj1450  33974  bnj1463  33979  bnj1529  33994  dvhvaddcbv  36691  dvhvaddval  36692  dvhopvadd  36695  dvhvaddcomN  36698  dvhvaddass  36699  dvhvscacbv  36700  dvhvscaval  36701  dvhopvsca  36704  dvhgrp  36709  dvhlveclem  36710  dvh0g  36713  dvhopaddN  36716  dvhopspN  36717  dvhopN  36718  cdlemn4  36800  hdmapffval  37431
  Copyright terms: Public domain W3C validator