Theorem preq2i 4737

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

Syntax hints:   = wceq 1534  {cpr 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-un 3950  df-sn 4625  df-pr 4627

This theorem is referenced by:  opidg  4888  funopg  6581  df2o2  8489  fz12pr  13584  fz0to3un2pr  13629  fz0to4untppr  13630  fzo13pr  13742  fzo0to2pr  13743  fzo0to42pr  13745  bpoly3  16028  prmreclem2  16879  2strstr1OLD  17199  mgmnsgrpex  18876  sgrpnmndex  18877  m2detleiblem2  22523  txindis  23531  setsvtx  28841  uhgrwkspthlem2  29561  31prm  46931  nnsum3primes4  47122  nnsum3primesgbe  47126