Theorem preq2i 4701

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

Syntax hints:   = wceq 1540  {cpr 4591

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  opidg  4856  funopg  6550  df2o2  8443  fz12pr  13542  fz0to3un2pr  13590  fz0to4untppr  13591  fzo13pr  13710  fzo0to2pr  13711  fz01pr  13712  fzo0to42pr  13714  bpoly3  16024  prmreclem2  16888  mgmnsgrpex  18858  sgrpnmndex  18859  m2detleiblem2  22515  txindis  23521  setsvtx  28962  uhgrwkspthlem2  29684  31prm  47598  nnsum3primes4  47789  nnsum3primesgbe  47793