Theorem preq2i 4670

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

Syntax hints:   = wceq 1539  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  opidg  4820  funopg  6452  df2o2  8283  fz12pr  13242  fz0to3un2pr  13287  fz0to4untppr  13288  fzo13pr  13399  fzo0to2pr  13400  fzo0to42pr  13402  bpoly3  15696  prmreclem2  16546  2strstr1OLD  16864  mgmnsgrpex  18485  sgrpnmndex  18486  m2detleiblem2  21685  txindis  22693  setsvtx  27308  uhgrwkspthlem2  28023  31prm  44937  nnsum3primes4  45128  nnsum3primesgbe  45132