Theorem preq2i 4681

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 4678	. 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
3	1, 2	ax-mp 5	1 ⊢ {𝐶, 𝐴} = {𝐶, 𝐵}

Syntax hints:   = wceq 1542  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  opidg  4835  funopg  6532  df2o2  8414  fz12pr  13535  fz0to3un2pr  13583  fz0to4untppr  13584  fzo13pr  13704  fzo0to2pr  13705  fz01pr  13706  fzo0to42pr  13708  bpoly3  16023  prmreclem2  16888  mgmnsgrpex  18902  sgrpnmndex  18903  m2detleiblem2  22593  txindis  23599  setsvtx  29104  uhgrwkspthlem2  29822  31prm  48060  nnsum3primes4  48264  nnsum3primesgbe  48268  gpg5edgnedg  48606