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

Theorem preq2i 4408
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 4405 . 2 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
31, 2ax-mp 5 1 {𝐶, 𝐴} = {𝐶, 𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  {cpr 4318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-sn 4317  df-pr 4319
This theorem is referenced by:  opidg  4558  funopg  6065  df2o2  7728  fzprval  12608  fz0to3un2pr  12649  fz0to4untppr  12650  fzo13pr  12760  fzo0to2pr  12761  fzo0to42pr  12763  bpoly3  14995  prmreclem2  15828  2strstr1  16194  mgmnsgrpex  17626  sgrpnmndex  17627  m2detleiblem2  20652  txindis  21658  iblcnlem1  23774  axlowdimlem4  26046  setsvtx  26148  uhgrwkspthlem2  26885  31prm  42040  nnsum3primes4  42204  nnsum3primesgbe  42208
  Copyright terms: Public domain W3C validator