Theorem preq2i 4704

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

Syntax hints:   = wceq 1540  {cpr 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-pr 4595

This theorem is referenced by:  opidg  4859  funopg  6553  df2o2  8446  fz12pr  13549  fz0to3un2pr  13597  fz0to4untppr  13598  fzo13pr  13717  fzo0to2pr  13718  fz01pr  13719  fzo0to42pr  13721  bpoly3  16031  prmreclem2  16895  mgmnsgrpex  18865  sgrpnmndex  18866  m2detleiblem2  22522  txindis  23528  setsvtx  28969  uhgrwkspthlem2  29691  31prm  47602  nnsum3primes4  47793  nnsum3primesgbe  47797