Theorem preq2i 4708

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

Syntax hints:   = wceq 1567  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4595  df-pr 4597

This theorem is referenced by:  opidg  4861  funopg  6571  df2o2  8461  fz12pr  13608  fz0to3un2pr  13656  fz0to4untppr  13657  fzo13pr  13777  fzo0to2pr  13778  fz01pr  13779  fzo0to42pr  13781  bpoly3  16111  prmreclem2  16976  mgmnsgrpex  18992  sgrpnmndex  18993  m2detleiblem2  22753  txindis  23759  setsvtx  29325  uhgrwkspthlem2  30043  31prm  48237  nnsum3primes4  48441  nnsum3primesgbe  48445  gpg5edgnedg  48783