Theorem preq2i 4696

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

Step	Hyp	Ref	Expression
1		preq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		preq2 4693	. 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
3	1, 2	ax-mp 5	1 ⊢ {𝐶, 𝐴} = {𝐶, 𝐵}

Syntax hints:   = wceq 1560  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-sn 4583  df-pr 4585

This theorem is referenced by:  opidg  4850  funopg  6555  df2o2  8446  fz12pr  13586  fz0to3un2pr  13634  fz0to4untppr  13635  fzo13pr  13755  fzo0to2pr  13756  fz01pr  13757  fzo0to42pr  13759  bpoly3  16088  prmreclem2  16953  mgmnsgrpex  18968  sgrpnmndex  18969  m2detleiblem2  22688  txindis  23694  setsvtx  29236  uhgrwkspthlem2  29954  31prm  48206  nnsum3primes4  48410  nnsum3primesgbe  48414  gpg5edgnedg  48752