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  6568  df2o2  8465  fz12pr  13637  fz0to3un2pr  13685  fz0to4untppr  13686  fzo13pr  13806  fzo0to2pr  13807  fz01pr  13808  fzo0to42pr  13810  bpoly3  16145  prmreclem2  17010  mgmnsgrpex  19044  sgrpnmndex  19045  m2detleiblem2  22851  txindis  23861  setsvtx  29493  uhgrwkspthlem2  30220  31prm  48501  nnsum3primes4  48705  nnsum3primesgbe  48709  gpg5edgnedg  49047