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

Theorem opeq12d 4198
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 4192 . 2  |-  ( ( A  =  B  /\  C  =  D )  -> 
<. A ,  C >.  = 
<. B ,  D >. )
41, 2, 3syl2anc 665 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   <.cop 4008
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009
This theorem is referenced by:  nfopd  4207  csbopg  4208  moop2  4716  fsn2g  6079  fnprb  6138  fnpr2g  6139  fliftfuns  6222  dfmpt2  6897  fsplit  6912  fnwelem  6922  seqomlem0  7174  seqomlem1  7175  seqomlem4  7178  qliftfuns  7458  xpassen  7672  xpdom2  7673  xpf1o  7740  xpmapenlem  7745  xpmapen  7746  mapunen  7747  xpwdomg  8100  fseqenlem2  8454  nqereu  9353  addpipq2  9360  addpipq  9361  mulpipq2  9363  mulpipq  9364  1nqenq  9386  mulidnq  9387  ltexnq  9399  prlem934  9457  addsrmo  9496  mulsrmo  9497  addsrpr  9498  mulsrpr  9499  mulcnsr  9559  mulresr  9562  axcnre  9587  om2uzrdg  12167  uzrdgsuci  12171  2swrd1eqwrdeq  12795  swrdswrd0  12803  ccatopth  12811  swrdccatin2d  12841  splval  12843  splcl  12844  cshfn  12877  repswcshw  12896  2swrd2eqwrdeq  13007  ruclem1  14261  eucalgval2  14511  qnumdenbi  14664  crt  14695  phimullem  14696  prmreclem3  14825  ressval3d  15148  imasval  15368  imasaddvallem  15386  xpsff1o  15425  catidex  15531  cidval  15534  catcocl  15542  catass  15543  oppccofval  15572  sectfval  15607  subccocl  15701  isfunc  15720  funcco  15727  idfuval  15732  idfucl  15737  cofuval  15738  cofuval2  15743  cofucl  15744  cofuass  15745  cofulid  15746  cofurid  15747  resfval  15748  resfval2  15749  funcres  15752  isnat  15803  nati  15811  fucco  15818  fuccoval  15819  coaval  15914  catcisolem  15952  xpcval  16013  xpcco  16019  xpcco2  16023  xpccatid  16024  xpcid  16025  1stfval  16027  2ndfval  16030  1stfcl  16033  2ndfcl  16034  prfval  16035  prf1  16036  prf2fval  16037  prf2  16038  prfcl  16039  prf1st  16040  prf2nd  16041  1st2ndprf  16042  xpcpropd  16044  evlfval  16053  evlf2  16054  evlfcllem  16057  evlfcl  16058  curfval  16059  curf1  16061  curf1cl  16064  curf2cl  16067  curfcl  16068  curfpropd  16069  uncf1  16072  uncf2  16073  curfuncf  16074  uncfcurf  16075  diagval  16076  curf2ndf  16083  hofval  16088  hof2fval  16091  hofcl  16095  yonval  16097  hofpropd  16103  yonedalem21  16109  yonedalem22  16114  yonedalem3  16116  symg2bas  16990  mat1dimmul  19432  txcnp  20566  upxp  20569  uptx  20571  hauseqlcld  20592  txlm  20594  txkgen  20598  cnmpt1t  20611  cnmpt2t  20619  txhmeo  20749  pt1hmeo  20752  flfcnp2  20953  ucnimalem  21226  ucnima  21227  fmucndlem  21237  fmucnd  21238  cnheiborlem  21878  pi1xfrcnvlem  21980  ovollb2lem  22319  ovollb2  22320  ovolshftlem2  22341  ovolscalem2  22345  ioombl1  22392  ioorf  22402  ioorval  22403  ioorinv2  22404  ioorfOLD  22407  ioorvalOLD  22408  ioorinv2OLD  22409  uniioombllem6  22423  dyadval  22427  opnmbl  22437  mbfimaopnlem  22488  limccnp2  22724  dvdsmulf1o  23986  ebtwntg  24858  usgrac  24924  numclwlk1lem2fv  25666  numclwlk1lem2fo  25668  hhssnvt  26751  hhsssh  26755  opfv  28087  xppreima  28088  aciunf1lem  28104  ofpreima  28108  fgreu  28114  smatlem  28462  fimaproj  28499  qtophaus  28502  qqhval2  28625  esum2dlem  28752  rrvadd  29111  bnj1442  29646  bnj1450  29647  bnj1463  29652  bnj1529  29667  erdszelem9  29710  erdszelem10  29711  txpcon  29743  txsconlem  29751  msubval  29951  msubco  29957  mvhval  29960  msubvrs  29986  poimirlem4  31648  opnmbllem0  31680  mblfinlem1  31681  mblfinlem2  31682  heiborlem6  31852  heiborlem7  31853  heiborlem8  31854  dvhvaddcbv  34366  dvhvaddval  34367  dvhopvadd  34370  dvhvaddcomN  34373  dvhvaddass  34374  dvhvscacbv  34375  dvhvscaval  34376  dvhopvsca  34379  dvhgrp  34384  dvhlveclem  34385  dvh0g  34388  dvhopaddN  34391  dvhopspN  34392  dvhopN  34393  cdlemn4  34475  hdmapffval  35106  pellexlem3  35385  pellex  35389  dvnprodlem1  37390  dvnprodlem3  37392  etransclem44  37710  aoveq123d  38070  pfxsuff1eqwrdeq  38338  inclfusubc  38625  funcrngcsetc  38758  funcrngcsetcALT  38759  funcringcsetc  38795
  Copyright terms: Public domain W3C validator