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

Theorem opeq12d 4225
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
opeq12d.2
Assertion
Ref Expression
opeq12d

Proof of Theorem opeq12d
StepHypRef Expression
1 opeq1d.1 . 2
2 opeq12d.2 . 2
3 opeq12 4219 . 2
41, 2, 3syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  <.cop 4035
This theorem is referenced by:  nfopd  4234  csbopg  4235  moop2  4747  fnprb  6129  fliftfuns  6212  dfmpt2  6890  fsplit  6905  fnwelem  6915  seqomlem0  7133  seqomlem1  7134  seqomlem4  7137  qliftfuns  7417  xpassen  7631  xpdom2  7632  xpf1o  7699  xpmapenlem  7704  xpmapen  7705  mapunen  7706  xpwdomg  8032  fseqenlem2  8427  nqereu  9328  addpipq2  9335  addpipq  9336  mulpipq2  9338  mulpipq  9339  1nqenq  9361  mulidnq  9362  ltexnq  9374  prlem934  9432  addsrmo  9471  mulsrmo  9472  addsrpr  9473  mulsrpr  9474  mulcnsr  9534  mulresr  9537  axcnre  9562  om2uzrdg  12067  uzrdgsuci  12071  2swrd1eqwrdeq  12679  swrdswrd0  12687  ccatopth  12695  swrdccatin2d  12725  splval  12727  splcl  12728  cshfn  12761  repswcshw  12780  2swrd2eqwrdeq  12891  ruclem1  13964  eucalgval2  14210  qnumdenbi  14277  crt  14308  phimullem  14309  prmreclem3  14436  imasval  14908  imasaddvallem  14926  xpsff1o  14965  catidex  15071  cidval  15074  catcocl  15082  catass  15083  oppccofval  15111  sectfval  15146  subccocl  15214  isfunc  15233  funcco  15240  idfuval  15245  idfucl  15250  cofuval  15251  cofuval2  15256  cofucl  15257  cofuass  15258  cofulid  15259  cofurid  15260  resfval  15261  resfval2  15262  funcres  15265  isnat  15316  nati  15324  fucco  15331  fuccoval  15332  coaval  15395  catcisolem  15433  xpcval  15446  xpcco  15452  xpcco2  15456  xpccatid  15457  xpcid  15458  1stfval  15460  2ndfval  15463  1stfcl  15466  2ndfcl  15467  prfval  15468  prf1  15469  prf2fval  15470  prf2  15471  prfcl  15472  prf1st  15473  prf2nd  15474  1st2ndprf  15475  xpcpropd  15477  evlfval  15486  evlf2  15487  evlfcllem  15490  evlfcl  15491  curfval  15492  curf1  15494  curf1cl  15497  curf2cl  15500  curfcl  15501  curfpropd  15502  uncf1  15505  uncf2  15506  curfuncf  15507  uncfcurf  15508  diagval  15509  curf2ndf  15516  hofval  15521  hof2fval  15524  hofcl  15528  yonval  15530  hofpropd  15536  yonedalem21  15542  yonedalem22  15547  yonedalem3  15549  symg2bas  16423  mat1dimmul  18978  txcnp  20121  upxp  20124  uptx  20126  hauseqlcld  20147  txlm  20149  txkgen  20153  cnmpt1t  20166  cnmpt2t  20174  txhmeo  20304  pt1hmeo  20307  flfcnp2  20508  ucnimalem  20783  ucnima  20784  fmucndlem  20794  fmucnd  20795  cnheiborlem  21454  pi1xfrcnvlem  21556  ovollb2lem  21899  ovollb2  21900  ovolshftlem2  21921  ovolscalem2  21925  ioombl1  21972  ioorf  21982  ioorval  21983  ioorinv2  21984  uniioombllem6  21997  dyadval  22001  opnmbl  22011  mbfimaopnlem  22062  limccnp2  22296  dvdsmulf1o  23470  ebtwntg  24285  usgrac  24351  numclwlk1lem2fv  25093  numclwlk1lem2fo  25095  hhssnvt  26181  hhsssh  26185  opfv  27486  xppreima  27487  ofpreima  27507  fgreu  27513  fimaproj  27836  qtophaus  27839  qqhval2  27963  rrvadd  28391  erdszelem9  28643  erdszelem10  28644  txpcon  28677  txsconlem  28685  msubval  28885  msubco  28891  mvhval  28894  msubvrs  28920  opnmbllem0  30050  mblfinlem1  30051  mblfinlem2  30052  heiborlem6  30312  heiborlem7  30313  heiborlem8  30314  pellexlem3  30767  pellex  30771  dvnprodlem1  31743  dvnprodlem3  31745  etransclem44  32061  aoveq123d  32263  ressval3d  32558  inclfusubc  32593  funcrngcsetc  32806  funcrngcsetcALT  32807  funcringcsetc  32843  bnj1442  34105  bnj1450  34106  bnj1463  34111  bnj1529  34126  dvhvaddcbv  36816  dvhvaddval  36817  dvhopvadd  36820  dvhvaddcomN  36823  dvhvaddass  36824  dvhvscacbv  36825  dvhvscaval  36826  dvhopvsca  36829  dvhgrp  36834  dvhlveclem  36835  dvh0g  36838  dvhopaddN  36841  dvhopspN  36842  dvhopN  36843  cdlemn4  36925  hdmapffval  37556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  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 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036
  Copyright terms: Public domain W3C validator