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

Theorem opeq12 4219
Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
Assertion
Ref Expression
opeq12

Proof of Theorem opeq12
StepHypRef Expression
1 opeq1 4217 . 2
2 opeq2 4218 . 2
31, 2sylan9eq 2518 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  <.cop 4035
This theorem is referenced by:  opeq12i  4222  opeq12d  4225  cbvopab  4520  opth  4726  copsex2t  4739  copsex2g  4740  relop  5158  funopg  5625  fvn0ssdmfun  6022  fsn  6069  fnressn  6083  fmptsng  6092  fmptsnd  6093  cbvoprab12  6371  eqopi  6834  f1o2ndf1  6908  tposoprab  7010  omeu  7253  brecop  7423  ecovcom  7436  ecovass  7437  ecovdi  7438  xpf1o  7699  addsrmo  9471  mulsrmo  9472  addsrpr  9473  mulsrpr  9474  addcnsr  9533  axcnre  9562  seqeq1  12110  fsumcnv  13588  fprodcnv  13787  eucalgval2  14210  xpstopnlem1  20310  qustgplem  20619  isrusgra  24927  qqhval2  27963  brsegle  29758  dvnprodlem1  31743  tpres  32554
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