Theorem preq2i 4697

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

Syntax hints:   = wceq 1540  {cpr 4587

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 3446  df-un 3916  df-sn 4586  df-pr 4588

This theorem is referenced by:  opidg  4852  funopg  6534  df2o2  8420  fz12pr  13518  fz0to3un2pr  13566  fz0to4untppr  13567  fzo13pr  13686  fzo0to2pr  13687  fz01pr  13688  fzo0to42pr  13690  bpoly3  16000  prmreclem2  16864  mgmnsgrpex  18834  sgrpnmndex  18835  m2detleiblem2  22491  txindis  23497  setsvtx  28938  uhgrwkspthlem2  29657  31prm  47571  nnsum3primes4  47762  nnsum3primesgbe  47766