Theorem preq2i 4633

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

Syntax hints:   = wceq 1538  {cpr 4527

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528

This theorem is referenced by:  opidg  4784  funopg  6358  df2o2  8101  fz12pr  12959  fz0to3un2pr  13004  fz0to4untppr  13005  fzo13pr  13116  fzo0to2pr  13117  fzo0to42pr  13119  bpoly3  15404  prmreclem2  16243  2strstr1  16597  mgmnsgrpex  18088  sgrpnmndex  18089  m2detleiblem2  21233  txindis  22239  setsvtx  26828  uhgrwkspthlem2  27543  31prm  44114  nnsum3primes4  44306  nnsum3primesgbe  44310