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 1542  {cpr 4584

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  opidg  4850  funopg  6534  df2o2  8416  fz12pr  13509  fz0to3un2pr  13557  fz0to4untppr  13558  fzo13pr  13677  fzo0to2pr  13678  fz01pr  13679  fzo0to42pr  13681  bpoly3  15993  prmreclem2  16857  mgmnsgrpex  18868  sgrpnmndex  18869  m2detleiblem2  22584  txindis  23590  setsvtx  29120  uhgrwkspthlem2  29839  31prm  47954  nnsum3primes4  48145  nnsum3primesgbe  48149  gpg5edgnedg  48487