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

Theorem preq2i 4672
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 4669 . 2 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
31, 2ax-mp 5 1 {𝐶, 𝐴} = {𝐶, 𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  {cpr 4566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-un 3945  df-sn 4565  df-pr 4567
This theorem is referenced by:  opidg  4821  funopg  6388  df2o2  8114  fz12pr  12959  fz0to3un2pr  13004  fz0to4untppr  13005  fzo13pr  13116  fzo0to2pr  13117  fzo0to42pr  13119  bpoly3  15407  prmreclem2  16248  2strstr1  16600  mgmnsgrpex  18041  sgrpnmndex  18042  m2detleiblem2  21172  txindis  22177  setsvtx  26753  uhgrwkspthlem2  27468  31prm  43611  nnsum3primes4  43804  nnsum3primesgbe  43808
  Copyright terms: Public domain W3C validator