Theorem preq2i 4694

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

Syntax hints:   = wceq 1541  {cpr 4582

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  opidg  4848  funopg  6526  df2o2  8406  fz12pr  13497  fz0to3un2pr  13545  fz0to4untppr  13546  fzo13pr  13665  fzo0to2pr  13666  fz01pr  13667  fzo0to42pr  13669  bpoly3  15981  prmreclem2  16845  mgmnsgrpex  18856  sgrpnmndex  18857  m2detleiblem2  22572  txindis  23578  setsvtx  29108  uhgrwkspthlem2  29827  31prm  47843  nnsum3primes4  48034  nnsum3primesgbe  48038  gpg5edgnedg  48376