Theorem preq2i 4703

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

Syntax hints:   = wceq 1541  {cpr 4593

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918  df-sn 4592  df-pr 4594

This theorem is referenced by:  opidg  4854  funopg  6540  df2o2  8426  fz12pr  13508  fz0to3un2pr  13553  fz0to4untppr  13554  fzo13pr  13666  fzo0to2pr  13667  fzo0to42pr  13669  bpoly3  15952  prmreclem2  16800  2strstr1OLD  17120  mgmnsgrpex  18755  sgrpnmndex  18756  m2detleiblem2  22014  txindis  23022  setsvtx  28049  uhgrwkspthlem2  28765  31prm  45909  nnsum3primes4  46100  nnsum3primesgbe  46104