Theorem preq2i 4762

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

Syntax hints:   = wceq 1537  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  opidg  4916  funopg  6612  df2o2  8531  fz12pr  13641  fz0to3un2pr  13686  fz0to4untppr  13687  fzo13pr  13800  fzo0to2pr  13801  fzo0to42pr  13803  bpoly3  16106  prmreclem2  16964  2strstr1OLD  17284  mgmnsgrpex  18966  sgrpnmndex  18967  m2detleiblem2  22655  txindis  23663  setsvtx  29070  uhgrwkspthlem2  29790  31prm  47471  nnsum3primes4  47662  nnsum3primesgbe  47666