Theorem preq2i 4669

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

Syntax hints:   = wceq 1547  {cpr 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4556  df-pr 4558

This theorem is referenced by:  opidg  4823  funopg  6519  df2o2  8404  fz12pr  13526  fz0to3un2pr  13574  fz0to4untppr  13575  fzo13pr  13695  fzo0to2pr  13696  fz01pr  13697  fzo0to42pr  13699  bpoly3  16014  prmreclem2  16879  mgmnsgrpex  18893  sgrpnmndex  18894  m2detleiblem2  22611  txindis  23617  setsvtx  29122  uhgrwkspthlem2  29840  31prm  48075  nnsum3primes4  48279  nnsum3primesgbe  48283  gpg5edgnedg  48621