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

Theorem opeq12d 4188
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 4182 . 2  |-  ( ( A  =  B  /\  C  =  D )  -> 
<. A ,  C >.  = 
<. B ,  D >. )
41, 2, 3syl2anc 671 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455   <.cop 3986
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987
This theorem is referenced by:  nfopd  4197  csbopg  4198  moop2  4710  fsn2g  6088  fnprb  6147  fntpb  6148  fnpr2g  6149  fliftfuns  6232  dfmpt2  6913  fsplit  6928  fnwelem  6938  seqomlem0  7192  seqomlem1  7193  seqomlem4  7196  qliftfuns  7476  xpassen  7692  xpdom2  7693  xpf1o  7760  xpmapenlem  7765  xpmapen  7766  mapunen  7767  xpwdomg  8126  fseqenlem2  8482  nqereu  9380  addpipq2  9387  addpipq  9388  mulpipq2  9390  mulpipq  9391  1nqenq  9413  mulidnq  9414  ltexnq  9426  prlem934  9484  addsrmo  9523  mulsrmo  9524  addsrpr  9525  mulsrpr  9526  mulcnsr  9586  mulresr  9589  axcnre  9614  om2uzrdg  12202  uzrdgsuci  12206  2swrd1eqwrdeq  12847  swrdswrd0  12855  ccatopth  12863  swrdccatin2d  12893  splval  12895  splcl  12896  cshfn  12929  repswcshw  12948  2swrd2eqwrdeq  13077  ruclem1  14332  eucalgval2  14589  qnumdenbi  14742  crt  14775  phimullem  14776  prmreclem3  14911  ressval3d  15235  imasval  15460  imasvalOLD  15461  imasaddvallem  15484  xpsff1o  15523  catidex  15629  cidval  15632  catcocl  15640  catass  15641  oppccofval  15670  sectfval  15705  subccocl  15799  isfunc  15818  funcco  15825  idfuval  15830  idfucl  15835  cofuval  15836  cofuval2  15841  cofucl  15842  cofuass  15843  cofulid  15844  cofurid  15845  resfval  15846  resfval2  15847  funcres  15850  isnat  15901  nati  15909  fucco  15916  fuccoval  15917  coaval  16012  catcisolem  16050  xpcval  16111  xpcco  16117  xpcco2  16121  xpccatid  16122  xpcid  16123  1stfval  16125  2ndfval  16128  1stfcl  16131  2ndfcl  16132  prfval  16133  prf1  16134  prf2fval  16135  prf2  16136  prfcl  16137  prf1st  16138  prf2nd  16139  1st2ndprf  16140  xpcpropd  16142  evlfval  16151  evlf2  16152  evlfcllem  16155  evlfcl  16156  curfval  16157  curf1  16159  curf1cl  16162  curf2cl  16165  curfcl  16166  curfpropd  16167  uncf1  16170  uncf2  16171  curfuncf  16172  uncfcurf  16173  diagval  16174  curf2ndf  16181  hofval  16186  hof2fval  16189  hofcl  16193  yonval  16195  hofpropd  16201  yonedalem21  16207  yonedalem22  16212  yonedalem3  16214  symg2bas  17088  mat1dimmul  19550  txcnp  20684  upxp  20687  uptx  20689  hauseqlcld  20710  txlm  20712  txkgen  20716  cnmpt1t  20729  cnmpt2t  20737  txhmeo  20867  pt1hmeo  20870  flfcnp2  21071  ucnimalem  21344  ucnima  21345  fmucndlem  21355  fmucnd  21356  cnheiborlem  22031  pi1xfrcnvlem  22136  ovollb2lem  22490  ovollb2  22491  ovolshftlem2  22512  ovolscalem2  22516  ioombl1  22564  ioorf  22574  ioorval  22575  ioorinv2  22576  ioorfOLD  22579  ioorvalOLD  22580  ioorinv2OLD  22581  uniioombllem6  22595  dyadval  22599  opnmbl  22609  mbfimaopnlem  22660  limccnp2  22896  dvdsmulf1o  24172  ebtwntg  25061  usgrac  25127  numclwlk1lem2fv  25870  numclwlk1lem2fo  25872  hhssnvt  26965  hhsssh  26969  opfv  28296  xppreima  28297  aciunf1lem  28313  ofpreima  28317  fgreu  28323  smatlem  28672  fimaproj  28709  qtophaus  28712  qqhval2  28835  esum2dlem  28962  rrvadd  29334  bnj1442  29907  bnj1450  29908  bnj1463  29913  bnj1529  29928  erdszelem9  29971  erdszelem10  29972  txpcon  30004  txsconlem  30012  msubval  30212  msubco  30218  mvhval  30221  msubvrs  30247  finxpreclem3  31830  poimirlem4  31989  opnmbllem0  32021  mblfinlem1  32022  mblfinlem2  32023  heiborlem6  32193  heiborlem7  32194  heiborlem8  32195  dvhvaddcbv  34702  dvhvaddval  34703  dvhopvadd  34706  dvhvaddcomN  34709  dvhvaddass  34710  dvhvscacbv  34711  dvhvscaval  34712  dvhopvsca  34715  dvhgrp  34720  dvhlveclem  34721  dvh0g  34724  dvhopaddN  34727  dvhopspN  34728  dvhopN  34729  cdlemn4  34811  hdmapffval  35442  pellexlem3  35720  pellex  35724  elcnvlem  36252  dvnprodlem1  37859  dvnprodlem3  37861  etransclem44  38181  aoveq123d  38718  pfxsuff1eqwrdeq  38988  iunopeqop  39045  funopsn  39060  inclfusubc  40140  funcrngcsetc  40273  funcrngcsetcALT  40274  funcringcsetc  40310
  Copyright terms: Public domain W3C validator