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

Theorem opeq12d 4079
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 4073 . 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 1369   <.cop 3895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896
This theorem is referenced by:  nfopd  4088  csbopg  4089  moop2  4598  fnprb  5948  fliftfuns  6019  dfmpt2  6675  fsplit  6689  fnwelem  6699  seqomlem0  6916  seqomlem1  6917  seqomlem4  6920  qliftfuns  7199  xpassen  7417  xpdom2  7418  xpf1o  7485  xpmapenlem  7490  xpmapen  7491  mapunen  7492  xpwdomg  7812  fseqenlem2  8207  nqereu  9110  addpipq2  9117  addpipq  9118  mulpipq2  9120  mulpipq  9121  1nqenq  9143  mulidnq  9144  ltexnq  9156  prlem934  9214  mulsrpr  9255  mulcnsr  9315  mulresr  9318  axcnre  9343  om2uzrdg  11791  uzrdgsuci  11795  2swrd1eqwrdeq  12360  swrdswrd0  12368  ccatopth  12376  swrdccatin2d  12403  splval  12405  splcl  12406  cshfn  12439  repswcshw  12458  2swrd2eqwrdeq  12565  ruclem1  13525  eucalgval2  13768  qnumdenbi  13834  crt  13865  phimullem  13866  prmreclem3  13991  imasval  14461  imasaddvallem  14479  xpsff1o  14518  catidex  14624  cidval  14627  catcocl  14635  catass  14636  oppccofval  14667  sectfval  14702  subccocl  14767  isfunc  14786  funcco  14793  idfuval  14798  idfucl  14803  cofuval  14804  cofuval2  14809  cofucl  14810  cofuass  14811  cofulid  14812  cofurid  14813  resfval  14814  resfval2  14815  funcres  14818  isnat  14869  nati  14877  fucco  14884  fuccoval  14885  coaval  14948  catcisolem  14986  xpcval  14999  xpcco  15005  xpcco2  15009  xpccatid  15010  xpcid  15011  1stfval  15013  2ndfval  15016  1stfcl  15019  2ndfcl  15020  prfval  15021  prf1  15022  prf2fval  15023  prf2  15024  prfcl  15025  prf1st  15026  prf2nd  15027  1st2ndprf  15028  xpcpropd  15030  evlfval  15039  evlf2  15040  evlfcllem  15043  evlfcl  15044  curfval  15045  curf1  15047  curf1cl  15050  curf2cl  15053  curfcl  15054  curfpropd  15055  uncf1  15058  uncf2  15059  curfuncf  15060  uncfcurf  15061  diagval  15062  curf2ndf  15069  hofval  15074  hof2fval  15077  hofcl  15081  yonval  15083  hofpropd  15089  yonedalem21  15095  yonedalem22  15100  yonedalem3  15102  symg2bas  15915  txcnp  19205  upxp  19208  uptx  19210  hauseqlcld  19231  txlm  19233  txkgen  19237  cnmpt1t  19250  cnmpt2t  19258  txhmeo  19388  pt1hmeo  19391  flfcnp2  19592  ucnimalem  19867  ucnima  19868  fmucndlem  19878  fmucnd  19879  cnheiborlem  20538  pi1xfrcnvlem  20640  ovollb2lem  20983  ovollb2  20984  ovolshftlem2  21005  ovolscalem2  21009  ioombl1  21055  ioorf  21065  ioorval  21066  ioorinv2  21067  uniioombllem6  21080  dyadval  21084  opnmbl  21094  mbfimaopnlem  21145  limccnp2  21379  dvdsmulf1o  22546  ebtwntg  23240  hhssnvt  24678  hhsssh  24682  opfv  25975  xppreima  25976  ofpreima  25996  fgreu  26002  qqhval2  26423  rrvadd  26847  erdszelem9  27099  erdszelem10  27100  txpcon  27133  txsconlem  27141  opnmbllem0  28439  mblfinlem1  28440  mblfinlem2  28441  heiborlem6  28727  heiborlem7  28728  heiborlem8  28729  pellexlem3  29184  pellex  29188  aoveq123d  30096  numclwlk1lem2fv  30698  numclwlk1lem2fo  30700  mat1dimmul  30884  bnj1442  32052  bnj1450  32053  bnj1463  32058  bnj1529  32073  dvhvaddcbv  34746  dvhvaddval  34747  dvhopvadd  34750  dvhvaddcomN  34753  dvhvaddass  34754  dvhvscacbv  34755  dvhvscaval  34756  dvhopvsca  34759  dvhgrp  34764  dvhlveclem  34765  dvh0g  34768  dvhopaddN  34771  dvhopspN  34772  dvhopN  34773  cdlemn4  34855  hdmapffval  35486
  Copyright terms: Public domain W3C validator