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

Theorem opeq2i 4221
Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
Hypothesis
Ref Expression
opeq1i.1
Assertion
Ref Expression
opeq2i

Proof of Theorem opeq2i
StepHypRef Expression
1 opeq1i.1 . 2
2 opeq2 4218 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  <.cop 4035
This theorem is referenced by:  fnressn  6083  fressnfv  6085  seqomlem1  7134  recmulnq  9363  addresr  9536  seqval  12118  ids1  12609  wrdeqs1cat  12700  swrdccat3a  12719  ressinbas  14693  oduval  15760  mgmnsgrpex  16049  sgrpnmndex  16050  efgi0  16738  efgi1  16739  vrgpinv  16787  frgpnabllem1  16877  mat1dimid  18976  clwlkfoclwwlk  24845  vdgr1c  24905  avril1  25171  ginvsn  25351  nvop  25580  phop  25733  signstfveq0  28534  wfrlem14  29356  zlmodzxzadd  32947  lmod1  33093  lmod1zr  33094  zlmodzxzequa  33097  zlmodzxzequap  33100  bnj601  33978  tgrpset  36471  erngset  36526  erngset-rN  36534
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