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

Theorem preq2i 4055
Description: Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
Hypothesis
Ref Expression
preq1i.1  |-  A  =  B
Assertion
Ref Expression
preq2i  |-  { C ,  A }  =  { C ,  B }

Proof of Theorem preq2i
StepHypRef Expression
1 preq1i.1 . 2  |-  A  =  B
2 preq2 4052 . 2  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
31, 2ax-mp 5 1  |-  { C ,  A }  =  { C ,  B }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405   {cpr 3974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-un 3419  df-sn 3973  df-pr 3975
This theorem is referenced by:  opid  4178  funopg  5601  df2o2  7181  fzprval  11795  fzo13pr  11935  fzo0to2pr  11936  fzo0to42pr  11938  bpoly3  14003  prmreclem2  14644  mgmnsgrpex  16373  sgrpnmndex  16374  m2detleiblem2  19422  txindis  20427  iblcnlem1  22486  axlowdimlem4  24665  usgraexvlem  24812  wlkntrllem2  24979  constr1trl  25007  constr3trllem3  25069  constr3pthlem1  25072  constr3pthlem3  25074  nnsum3primes4  37836  nnsum3primesgbe  37840
  Copyright terms: Public domain W3C validator