Theorem preq2i 4691

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

Syntax hints:   = wceq 1540  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-sn 4580  df-pr 4582

This theorem is referenced by:  opidg  4846  funopg  6520  df2o2  8404  fz12pr  13503  fz0to3un2pr  13551  fz0to4untppr  13552  fzo13pr  13671  fzo0to2pr  13672  fz01pr  13673  fzo0to42pr  13675  bpoly3  15984  prmreclem2  16848  mgmnsgrpex  18824  sgrpnmndex  18825  m2detleiblem2  22532  txindis  23538  setsvtx  28999  uhgrwkspthlem2  29718  31prm  47601  nnsum3primes4  47792  nnsum3primesgbe  47796  gpg5edgnedg  48134