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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  opidg  4852  funopg  6567  df2o2  8464  fz12pr  13636  fz0to3un2pr  13684  fz0to4untppr  13685  fzo13pr  13805  fzo0to2pr  13806  fz01pr  13807  fzo0to42pr  13809  bpoly3  16144  prmreclem2  17009  mgmnsgrpex  19043  sgrpnmndex  19044  m2detleiblem2  22850  txindis  23860  setsvtx  29492  uhgrwkspthlem2  30219  31prm  48500  nnsum3primes4  48704  nnsum3primesgbe  48708  gpg5edgnedg  49046