Theorem preq2i 4216

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

Syntax hints:   = wceq 1475  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128

This theorem is referenced by:  opid  4359  funopg  5836  df2o2  7461  fzprval  12271  fz0to3un2pr  12310  fz0to4untppr  12311  fzo13pr  12419  fzo0to2pr  12420  fzo0to42pr  12422  bpoly3  14628  prmreclem2  15459  2strstr1  15812  mgmnsgrpex  17241  sgrpnmndex  17242  m2detleiblem2  20253  txindis  21247  iblcnlem1  23360  axlowdimlem4  25625  wlkntrllem2  26090  constr1trl  26118  constr3trllem3  26180  constr3pthlem1  26183  constr3pthlem3  26185  31prm  40050  nnsum3primes4  40204  nnsum3primesgbe  40208  opidg  40316  uhgr1wlkspthlem2  40960