Theorem preq2i 4682

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

Syntax hints:   = wceq 1542  {cpr 4570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  opidg  4836  funopg  6526  df2o2  8407  fz12pr  13526  fz0to3un2pr  13574  fz0to4untppr  13575  fzo13pr  13695  fzo0to2pr  13696  fz01pr  13697  fzo0to42pr  13699  bpoly3  16014  prmreclem2  16879  mgmnsgrpex  18893  sgrpnmndex  18894  m2detleiblem2  22603  txindis  23609  setsvtx  29118  uhgrwkspthlem2  29837  31prm  48072  nnsum3primes4  48276  nnsum3primesgbe  48280  gpg5edgnedg  48618