Theorem preq2i 4634

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

Syntax hints:   = wceq 1539  {cpr 4528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-un 3866  df-sn 4527  df-pr 4529

This theorem is referenced by:  opidg  4786  funopg  6375  df2o2  8135  fz12pr  13027  fz0to3un2pr  13072  fz0to4untppr  13073  fzo13pr  13184  fzo0to2pr  13185  fzo0to42pr  13187  bpoly3  15474  prmreclem2  16323  2strstr1  16678  mgmnsgrpex  18177  sgrpnmndex  18178  m2detleiblem2  21343  txindis  22349  setsvtx  26942  uhgrwkspthlem2  27657  31prm  44542  nnsum3primes4  44733  nnsum3primesgbe  44737