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

Theorem preq2i 4113
Description: Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
Hypothesis
Ref Expression
preq1i.1
Assertion
Ref Expression
preq2i

Proof of Theorem preq2i
StepHypRef Expression
1 preq1i.1 . 2
2 preq2 4110 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  {cpr 4031
This theorem is referenced by:  opid  4236  funopg  5625  df2o2  7163  fzprval  11769  fzo0to2pr  11899  fzo0to42pr  11901  prmreclem2  14435  mgmnsgrpex  16049  sgrpnmndex  16050  m2detleiblem2  19130  txindis  20135  iblcnlem1  22194  axlowdimlem4  24248  usgraexvlem  24395  wlkntrllem2  24562  constr1trl  24590  constr3trllem3  24652  constr3pthlem1  24655  constr3pthlem3  24657  bpoly3  29820
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-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032
  Copyright terms: Public domain W3C validator