Theorem preq2d 4721

Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)

Hypothesis

Ref	Expression
preq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
preq2d	⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})

Proof of Theorem preq2d

Step	Hyp	Ref	Expression
1		preq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		preq2 4715	. 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})

Syntax hints:   → wi 4   = wceq 1540  {cpr 4608

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-sn 4607  df-pr 4609

This theorem is referenced by:  opeq2  4855  opthwiener  5494  fprg  7150  fprb  7191  fnprb  7205  fnpr2g  7207  opthreg  9637  fzosplitprm1  13798  s2prop  14931  gsumprval  18671  indislem  22943  isconn  23356  hmphindis  23740  wilthlem2  27036  ispth  29708  wwlksnredwwlkn  29882  wwlksnextfun  29885  wwlksnextinj  29886  wwlksnextsurj  29887  wwlksnextbij  29889  clwlkclwwlklem2a1  29978  clwlkclwwlklem2a4  29983  clwlkclwwlklem2  29986  clwwisshclwwslemlem  29999  clwwlkn2  30030  clwwlkf  30033  clwwlknonex2lem1  30093  eupth2lem3lem3  30216  eupth2  30225  frcond1  30252  nfrgr2v  30258  frgr3v  30261  n4cyclfrgr  30277  measxun2  34246  altopthsn  35984  mapdindp4  41747  clnbgrgrimlem  47913  gpgov  48013  gpgprismgriedgdmss  48023  gpg3kgrtriexlem6  48057  gpgprismgr4cycllem3  48063  2arymaptf1  48600  rrx2xpref1o  48665