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

Theorem preq2i 4634
 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 4631 . 2 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
31, 2ax-mp 5 1 {𝐶, 𝐴} = {𝐶, 𝐵}
 Colors of variables: wff setvar class Syntax hints:   = wceq 1539  {cpr 4528 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-un 3866  df-sn 4527  df-pr 4529 This theorem is referenced by:  opidg  4786  funopg  6375  df2o2  8135  fz12pr  13027  fz0to3un2pr  13072  fz0to4untppr  13073  fzo13pr  13184  fzo0to2pr  13185  fzo0to42pr  13187  bpoly3  15474  prmreclem2  16323  2strstr1  16678  mgmnsgrpex  18177  sgrpnmndex  18178  m2detleiblem2  21343  txindis  22349  setsvtx  26942  uhgrwkspthlem2  27657  31prm  44542  nnsum3primes4  44733  nnsum3primesgbe  44737
 Copyright terms: Public domain W3C validator