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 1541  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4578  df-pr 4580

This theorem is referenced by:  opidg  4845  funopg  6523  df2o2  8403  fz12pr  13488  fz0to3un2pr  13536  fz0to4untppr  13537  fzo13pr  13656  fzo0to2pr  13657  fz01pr  13658  fzo0to42pr  13660  bpoly3  15972  prmreclem2  16836  mgmnsgrpex  18847  sgrpnmndex  18848  m2detleiblem2  22563  txindis  23569  setsvtx  29034  uhgrwkspthlem2  29753  31prm  47759  nnsum3primes4  47950  nnsum3primesgbe  47954  gpg5edgnedg  48292