Theorem preq2i 4703

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

Syntax hints:   = wceq 1570  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4590  df-pr 4592

This theorem is referenced by:  opidg  4857  funopg  6570  df2o2  8458  fz12pr  13605  fz0to3un2pr  13653  fz0to4untppr  13654  fzo13pr  13774  fzo0to2pr  13775  fz01pr  13776  fzo0to42pr  13778  bpoly3  16107  prmreclem2  16972  mgmnsgrpex  18988  sgrpnmndex  18989  m2detleiblem2  22785  txindis  23791  setsvtx  29385  uhgrwkspthlem2  30103  31prm  48349  nnsum3primes4  48553  nnsum3primesgbe  48557  gpg5edgnedg  48895