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

Theorem opeq2d 4224
Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
Hypothesis
Ref Expression
opeq1d.1
Assertion
Ref Expression
opeq2d

Proof of Theorem opeq2d
StepHypRef Expression
1 opeq1d.1 . 2
2 opeq2 4218 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  <.cop 4035
This theorem is referenced by:  fmptsng  6092  fmptsnd  6093  tfrlem11  7076  seqomlem0  7133  seqomlem1  7134  seqomlem4  7137  seqomeq12  7138  fundmen  7609  unxpdomlem1  7744  mulcanenq  9359  elreal2  9530  om2uzrdg  12067  uzrdgsuci  12071  seqeq2  12111  seqeq3  12112  s1val  12610  s1eq  12612  swrdlsw  12677  swrdccatwrd  12693  ccats1swrdeq  12694  ccatopth  12695  wrdeqcats1  12699  swrdccat  12718  swrdccat3blem  12720  swrdccat3b  12721  swrdccatin12d  12726  splval  12727  splcl  12728  cshfn  12761  cshw0  12765  cshwmodn  12766  repswcshw  12780  swrds2  12883  swrd2lsw  12890  eucalgval  14211  ressval  14684  ressress  14694  prdsval  14852  imasval  14908  imasaddvallem  14926  cidval  15074  iscatd2  15078  oppcval  15108  ismon  15128  rescval  15196  idfucl  15250  funcres  15265  fucval  15327  fucpropd  15346  setcval  15404  catcval  15423  xpcval  15446  1stfcl  15466  2ndfcl  15467  curf12  15496  curf2val  15499  curfcl  15501  hofcl  15528  oduval  15760  ipoval  15784  frmdval  16019  oppgval  16382  symgval  16404  efgmval  16730  efgmnvl  16732  efgi  16737  frgpup3lem  16795  dprd2da  17091  dmdprdpr  17098  dprdpr  17099  pgpfaclem1  17132  mgpval  17144  mgpress  17152  opprval  17273  sraval  17822  rlmval2  17840  psrval  18011  opsrval  18139  opsrval2  18141  zlmval  18553  znval  18572  znval2  18576  thlval  18726  islindf4  18873  matval  18913  mat1dimmul  18978  mat1dimcrng  18979  mat1scmat  19041  mdet0pr  19094  m1detdiag  19099  txkgen  20153  pt1hmeo  20307  xpstopnlem1  20310  tusval  20769  tmsval  20984  tngval  21153  om1val  21530  pi1xfrcnvlem  21556  pi1xfrcnv  21557  dchrval  23509  ttgval  24178  eengv  24282  wwlkextwrd  24728  wwlkextproplem3  24743  clwlkisclwwlk2  24790  clwwlkf1  24796  clwlkfoclwwlk  24845  clwlkf1clwwlklem  24849  clwlkf1clwwlk  24850  clwlksizeeq  24852  eupath2lem3  24979  numclwlk1lem2f1  25094  numclwlk2lem2f1o  25105  br8d  27463  resvval  27817  fvproj  27835  qqhval  27955  iwrdsplit  28326  subfacp1lem5  28628  cvmliftlem10  28739  cvmlift2lem12  28759  msubffval  28883  msubfval  28884  elmsubrn  28888  msubrn  28889  msubco  28891  br8  29185  br6  29186  btwnouttr2  29672  brfs  29729  btwnconn1lem11  29747  finixpnum  30038  mendval  31132  setsidvald  32557  idfusubc0  32591  idfusubc  32592  estrcval  32630  rngcvalOLD  32769  ringcvalOLD  32815  zlmodzxzsub  32949  lmod1zr  33094  bnj66  33918  bnj1234  34069  bnj1296  34077  bnj1450  34106  bnj1463  34111  bnj1501  34123  bnj1523  34127  ldualset  34850  tgrpfset  36470  tgrpset  36471  erngfset  36525  erngset  36526  erngfset-rN  36533  erngset-rN  36534  dvafset  36730  dvaset  36731  dvhfset  36807  dvhset  36808  dvhfvadd  36818  dvhopvadd2  36821  dib1dim2  36895  dicvscacl  36918  cdlemn6  36929  dihopelvalcpre  36975  dih1dimatlem  37056  hdmapfval  37557  hlhilset  37664
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