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

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

Proof of Theorem opeq1d
StepHypRef Expression
1 opeq1d.1 . 2
2 opeq1 4217 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  <.cop 4035
This theorem is referenced by:  oteq1  4226  oteq2  4227  opth  4726  cbvoprab2  6370  unxpdomlem1  7744  mulcanenq  9359  ax1rid  9559  axrnegex  9560  fseq1m1p1  11782  uzrdglem  12068  swrd0swrd  12686  swrdccat  12718  swrdccat3a  12719  swrdccat3blem  12720  cshw0  12765  cshwmodn  12766  s2prop  12862  s4prop  12863  fsum2dlem  13585  fprod2dlem  13784  ruclem1  13964  imasaddvallem  14926  iscatd2  15078  moni  15131  homadmcd  15369  curf1  15494  curf1cl  15497  curf2  15498  hofcl  15528  gsum2dlem2  16998  gsum2dOLD  17000  mat1dimmul  18978  imasdsf1olem  20876  ovoliunlem1  21913  cxpcn3  23122  axlowdimlem15  24259  axlowdim  24264  nvi  25507  nvop  25580  phop  25733  br8d  27463  fgreu  27513  fvproj  27835  mvhfval  28893  mpst123  28900  br8  29185  fvtransport  29682
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