Theorem preq2i 4742

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

Syntax hints:   = wceq 1539  {cpr 4631

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3954  df-sn 4630  df-pr 4632

This theorem is referenced by:  opidg  4893  funopg  6583  df2o2  8479  fz12pr  13564  fz0to3un2pr  13609  fz0to4untppr  13610  fzo13pr  13722  fzo0to2pr  13723  fzo0to42pr  13725  bpoly3  16008  prmreclem2  16856  2strstr1OLD  17176  mgmnsgrpex  18850  sgrpnmndex  18851  m2detleiblem2  22352  txindis  23360  setsvtx  28560  uhgrwkspthlem2  29276  31prm  46565  nnsum3primes4  46756  nnsum3primesgbe  46760