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

Theorem preq2i 4263
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 4260 . 2 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
31, 2ax-mp 5 1 {𝐶, 𝐴} = {𝐶, 𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  {cpr 4170
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-un 3572  df-sn 4169  df-pr 4171
This theorem is referenced by:  opid  4412  funopg  5910  df2o2  7559  fzprval  12386  fz0to3un2pr  12425  fz0to4untppr  12426  fzo13pr  12536  fzo0to2pr  12537  fzo0to42pr  12539  bpoly3  14770  prmreclem2  15602  2strstr1  15967  mgmnsgrpex  17399  sgrpnmndex  17400  m2detleiblem2  20415  txindis  21418  iblcnlem1  23535  axlowdimlem4  25806  setsvtx  25908  uhgrwkspthlem2  26631  opidg  41060  31prm  41277  nnsum3primes4  41441  nnsum3primesgbe  41445
  Copyright terms: Public domain W3C validator