Theorem preq2i 4694

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

This proof depends on syntax axioms:   = wceq 1569  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150  df-sn 4585  df-pr 4587

This theorem is used by:  opidg  4851  funopg  6579  df2o2  8493  fz12pr  13722  fz0to3un2pr  13770  fz0to4untppr  13771  fzo13pr  13891  fzo0to2pr  13892  fz01pr  13893  fzo0to42pr  13895  bpoly3  16233  mgmnsgrpex  19139  sgrpnmndex  19140  m2detleiblem2  22952  txindis  23962  setsvtx  29622  31prm  48818  nnsum3primes4  49022  nnsum3primesgbe  49026  gpg5edgnedg  49364