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

Theorem preq2i 4461
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 4458 . 2 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
31, 2ax-mp 5 1 {𝐶, 𝐴} = {𝐶, 𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1653  {cpr 4370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-un 3774  df-sn 4369  df-pr 4371
This theorem is referenced by:  opidg  4612  funopg  6135  df2o2  7814  fzprval  12655  fz0to3un2pr  12696  fz0to4untppr  12697  fzo13pr  12807  fzo0to2pr  12808  fzo0to42pr  12810  bpoly3  15125  prmreclem2  15954  2strstr1  16307  mgmnsgrpex  17734  sgrpnmndex  17735  m2detleiblem2  20760  txindis  21766  iblcnlem1  23895  axlowdimlem4  26182  setsvtx  26270  uhgrwkspthlem2  27008  31prm  42294  nnsum3primes4  42458  nnsum3primesgbe  42462
  Copyright terms: Public domain W3C validator