Theorem preq2d 4694

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 4688	. 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})

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

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 3440  df-un 3910  df-sn 4580  df-pr 4582

This theorem is referenced by:  opeq2  4828  opthwiener  5461  fprg  7093  fprb  7134  fnprb  7148  fnpr2g  7150  opthreg  9533  fzosplitprm1  13698  s2prop  14832  gsumprval  18580  indislem  22903  isconn  23316  hmphindis  23700  wilthlem2  26995  ispth  29684  wwlksnredwwlkn  29858  wwlksnextfun  29861  wwlksnextinj  29862  wwlksnextsurj  29863  wwlksnextbij  29865  clwlkclwwlklem2a1  29954  clwlkclwwlklem2a4  29959  clwlkclwwlklem2  29962  clwwisshclwwslemlem  29975  clwwlkn2  30006  clwwlkf  30009  clwwlknonex2lem1  30069  eupth2lem3lem3  30192  eupth2  30201  frcond1  30228  nfrgr2v  30234  frgr3v  30237  n4cyclfrgr  30253  measxun2  34176  altopthsn  35934  mapdindp4  41702  clnbgrgrimlem  47918  gpgov  48027  gpgprismgriedgdmss  48037  gpgedg2ov  48051  gpgedg2iv  48052  gpg3kgrtriexlem6  48073  gpgprismgr4cycllem3  48082  grlimedgnedg  48116  2arymaptf1  48639  rrx2xpref1o  48704