Theorem preq2i 4698

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

This proof depends on syntax axioms:   = wceq 1570  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  opidg  4852  funopg  6574  df2o2  8485  fz12pr  13715  fz0to3un2pr  13763  fz0to4untppr  13764  fzo13pr  13884  fzo0to2pr  13885  fz01pr  13886  fzo0to42pr  13888  bpoly3  16224  prmreclem2  17095  mgmnsgrpex  19130  sgrpnmndex  19131  m2detleiblem2  22943  txindis  23953  setsvtx  29613  uhgrwkspthlem2  30340  31prm  48681  nnsum3primes4  48885  nnsum3primesgbe  48889  gpg5edgnedg  49227